harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/IsDiag.lean
theorem IsDiag.fromBlocks [Zero α] {A : Matrix m m α} {D : Matrix n n α} (ha : A.IsDiag)
    (hd : D.IsDiag) : (A.fromBlocks 0 0 D).IsDiag

Proof state:
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
⊢ (Matrix.fromBlocks A 0 0 D).IsDiag

Tactic:
rintro (i | i) (j | j) hij

Result:
case inl.inl
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i j : m
hij : Sum.inl i ≠ Sum.inl j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inl i) (Sum.inl j) = 0

case inl.inr
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i : m
j : n
hij : Sum.inl i ≠ Sum.inr j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inl i) (Sum.inr j) = 0

case inr.inl
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i : n
j : m
hij : Sum.inr i ≠ Sum.inl j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inr i) (Sum.inl j) = 0

case inr.inr
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i j : n
hij : Sum.inr i ≠ Sum.inr j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inr i) (Sum.inr j) = 0

Proof state:
case inr.inl
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i : n
j : m
hij : Sum.inr i ≠ Sum.inl j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inr i) (Sum.inl j) = 0

Tactic:
rfl

Result:
no goals

Proof state:
case inl.inr
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i : m
j : n
hij : Sum.inl i ≠ Sum.inr j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inl i) (Sum.inr j) = 0

Tactic:
rfl

Result:
no goals

Proof state:
case inl.inl
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i j : m
hij : Sum.inl i ≠ Sum.inl j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inl i) (Sum.inl j) = 0

Tactic:
exact ha (ne_of_apply_ne _ hij)

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i j : n
hij : Sum.inr i ≠ Sum.inr j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inr i) (Sum.inr j) = 0

Tactic:
exact hd (ne_of_apply_ne _ hij)

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem stoppedValue_lowerCrossingTime (h : lowerCrossingTime a b f N n ω ≠ N) :
    stoppedValue f (lowerCrossingTime a b f N n) ω ≤ a

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : lowerCrossingTime a b f N n ω ≠ N
⊢ stoppedValue f (lowerCrossingTime a b f N n) ω ≤ a

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := (hitting_le_iff_of_lt _ (lt_of_le_of_ne lowerCrossingTime_le h)).1 le_rfl

Result:
case intro.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : lowerCrossingTime a b f N n ω ≠ N
j : ℕ
hj₁ : j ∈ Set.Icc (upperCrossingTime a b f N n ω) (lowerCrossingTime a b f N n ω)
hj₂ : f j ω ∈ Set.Iic a
⊢ stoppedValue f (lowerCrossingTime a b f N n) ω ≤ a

Proof state:
case intro.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : lowerCrossingTime a b f N n ω ≠ N
j : ℕ
hj₁ : j ∈ Set.Icc (upperCrossingTime a b f N n ω) (lowerCrossingTime a b f N n ω)
hj₂ : f j ω ∈ Set.Iic a
⊢ stoppedValue f (lowerCrossingTime a b f N n) ω ≤ a

Tactic:
exact stoppedValue_hitting_mem ⟨j, ⟨hj₁.1, le_trans hj₁.2 lowerCrossingTime_le⟩, hj₂⟩

Result:
no goals
-- Mathlib/NumberTheory/Modular.lean
theorem re_T_smul : (T • z).re = z.re + 1

Proof state:
z : ℍ
⊢ (T • z).re = z.re + 1

Tactic:
simpa using re_T_zpow_smul z 1

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem sup_eq_closure (H H' : Subgroup G) : H ⊔ H' = closure ((H : Set G) ∪ (H' : Set G))

Proof state:
G : Type u_1
inst✝ : Group G
H H' : Subgroup G
⊢ H ⊔ H' = closure (↑H ∪ ↑H')

Tactic:
simp_rw [closure_union, closure_eq]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_pow (z : ℤ_[p]) : ∀ n : ℕ, ‖z ^ n‖ = ‖z‖ ^ n
  | 0 => by simp
  | k + 1 => by
    rw [pow_succ, pow_succ, norm_mul]
    congr
    apply norm_pow

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ‖z ^ 0‖ = ‖z‖ ^ 0

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
k : ℕ
⊢ ‖z ^ k‖ * ‖z‖ = ‖z‖ ^ k * ‖z‖

Tactic:
congr

Result:
case e_a
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
k : ℕ
⊢ ‖z ^ k‖ = ‖z‖ ^ k

Proof state:
case e_a
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
k : ℕ
⊢ ‖z ^ k‖ = ‖z‖ ^ k

Tactic:
apply norm_pow

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
k : ℕ
⊢ ‖z ^ (k + 1)‖ = ‖z‖ ^ (k + 1)

Tactic:
rw [pow_succ, pow_succ, norm_mul]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
k : ℕ
⊢ ‖z ^ k‖ * ‖z‖ = ‖z‖ ^ k * ‖z‖
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_pos_of_not_dvd {a b : Int} (h : ¬ a ∣ b) : a = 0 ∨ 0 < b % a

Proof state:
a b : Int
h : ¬b % a = 0
⊢ a = 0 ∨ 0 < b % a

Tactic:
by_cases w : a = 0

Result:
case pos
a b : Int
h : ¬b % a = 0
w : a = 0
⊢ a = 0 ∨ 0 < b % a

case neg
a b : Int
h : ¬b % a = 0
w : ¬a = 0
⊢ a = 0 ∨ 0 < b % a

Proof state:
case neg
a b : Int
h : ¬b % a = 0
w : ¬a = 0
⊢ a = 0 ∨ 0 < b % a

Tactic:
exact Or.inr (Int.lt_iff_le_and_ne.mpr ⟨emod_nonneg b w, Ne.symm h⟩)

Result:
no goals

Proof state:
case pos
a b : Int
h : ¬b % a = 0
w : a = 0
⊢ a = 0 ∨ 0 < b % a

Tactic:
simp_all

Result:
no goals

Proof state:
a b : Int
h : ¬a ∣ b
⊢ a = 0 ∨ 0 < b % a

Tactic:
rw [dvd_iff_emod_eq_zero] at h

Result:
a b : Int
h : ¬b % a = 0
⊢ a = 0 ∨ 0 < b % a
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem derivativeFun_add (f g : R⟦X⟧) :
    derivativeFun (f + g) = derivativeFun f + derivativeFun g

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
f g : R⟦X⟧
n✝ : ℕ
⊢ (coeff R n✝) (f + g).derivativeFun = (coeff R n✝) (f.derivativeFun + g.derivativeFun)

Tactic:
rw [coeff_derivativeFun, map_add, map_add, coeff_derivativeFun,
  coeff_derivativeFun, add_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : R⟦X⟧
⊢ (f + g).derivativeFun = f.derivativeFun + g.derivativeFun

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
f g : R⟦X⟧
n✝ : ℕ
⊢ (coeff R n✝) (f + g).derivativeFun = (coeff R n✝) (f.derivativeFun + g.derivativeFun)
-- Mathlib/Analysis/Normed/Ring/Seminorm.lean
/-- Equivalence of multiplicative ring norms is reflexive. -/
@[deprecated "Use AbsoluteValue.isEquiv_refl instead" (since := "2025-01-07")]
lemma equiv_refl (f : MulRingNorm R) : equiv f f

Proof state:
R : Type u_2
inst✝ : Ring R
f : MulRingNorm R
⊢ f.equiv f

Tactic:
exact ⟨1, Real.zero_lt_one, by simp only [Real.rpow_one]⟩

Result:
no goals

Proof state:
R : Type u_2
inst✝ : Ring R
f : MulRingNorm R
⊢ (fun x => f x ^ 1) = ⇑f

Tactic:
simp only [Real.rpow_one]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_eq_prod (f : α → M) {s : Set α} (hf : (s ∩ mulSupport f).Finite) :
    ∏ᶠ i ∈ s, f i = ∏ i ∈ hf.toFinset, f i :=
  finprod_mem_eq_prod_of_inter_mulSupport_eq _ <| by simp [inter_assoc]

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hf : (s ∩ mulSupport f).Finite
⊢ s ∩ mulSupport f = ↑hf.toFinset ∩ mulSupport f

Tactic:
simp [inter_assoc]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem dvdNotUnit_of_lt {a b : Associates M} (hlt : a < b) : DvdNotUnit a b

Proof state:
case right.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : ¬a * x ∣ a
⊢ ∃ x_1, ¬IsUnit x_1 ∧ a * x = a * x_1

Tactic:
refine ⟨x, ?_, rfl⟩

Result:
case right.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : ¬a * x ∣ a
⊢ ¬IsUnit x

Proof state:
case right.intro.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
u : (Associates M)ˣ
⊢ a * ↑u ∣ a

Tactic:
simp

Result:
no goals

Proof state:
case left
M : Type u_1
inst✝ : CommMonoidWithZero M
b : Associates M
hlt : 0 < b
⊢ False

Tactic:
apply not_lt_of_le _ hlt

Result:
M : Type u_1
inst✝ : CommMonoidWithZero M
b : Associates M
hlt : 0 < b
⊢ b ≤ 0

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
b : Associates M
hlt : 0 < b
⊢ b ≤ 0

Tactic:
apply dvd_zero

Result:
no goals

Proof state:
case right.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : ¬a * x ∣ a
⊢ ¬IsUnit x

Tactic:
contrapose! ndvd

Result:
case right.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : IsUnit x
⊢ a * x ∣ a

Proof state:
case right.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : IsUnit x
⊢ a * x ∣ a

Tactic:
rcases ndvd with ⟨u, rfl⟩

Result:
case right.intro.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
u : (Associates M)ˣ
⊢ a * ↑u ∣ a

Proof state:
case left
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : Associates M
hlt : a < b
⊢ a ≠ 0

Tactic:
rintro rfl

Result:
case left
M : Type u_1
inst✝ : CommMonoidWithZero M
b : Associates M
hlt : 0 < b
⊢ False

Proof state:
case right
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : Associates M
hlt : a < b
⊢ ∃ x, ¬IsUnit x ∧ b = a * x

Tactic:
rcases hlt with ⟨⟨x, rfl⟩, ndvd⟩

Result:
case right.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : ¬a * x ∣ a
⊢ ∃ x_1, ¬IsUnit x_1 ∧ a * x = a * x_1

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : Associates M
hlt : a < b
⊢ DvdNotUnit a b

Tactic:
constructor

Result:
case left
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : Associates M
hlt : a < b
⊢ a ≠ 0

case right
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : Associates M
hlt : a < b
⊢ ∃ x, ¬IsUnit x ∧ b = a * x
-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem exists_rat_eq_nth_num : ∃ q : ℚ, (of v).nums n = (q : K)

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ q, (of v).nums n = ↑q

Tactic:
rcases exists_gcf_pair_rat_eq_nth_conts v n with ⟨⟨a, _⟩, nth_cont_eq⟩

Result:
case intro.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a b✝ : ℚ
nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a, b := b✝ }
⊢ ∃ q, (of v).nums n = ↑q

Proof state:
case intro.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a b✝ : ℚ
nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a, b := b✝ }
⊢ ∃ q, (of v).nums n = ↑q

Tactic:
use a

Result:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a b✝ : ℚ
nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a, b := b✝ }
⊢ (of v).nums n = ↑a

Proof state:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a b✝ : ℚ
nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a, b := b✝ }
⊢ (of v).nums n = ↑a

Tactic:
simp [num_eq_conts_a, nth_cont_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem add_lintegral (f g : α →ₛ ℝ≥0∞) : (f + g).lintegral μ = f.lintegral μ + g.lintegral μ :=
  calc
    (f + g).lintegral μ =
        ∑ x ∈ (pair f g).range, (x.1 * μ (pair f g ⁻¹' {x}) + x.2 * μ (pair f g ⁻¹' {x}))

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x ∈ (f.pair g).range, (x.1 * μ (⇑(f.pair g) ⁻¹' {x}) + x.2 * μ (⇑(f.pair g) ⁻¹' {x})) =
    ∑ x ∈ (f.pair g).range, x.1 * μ (⇑(f.pair g) ⁻¹' {x}) + ∑ x ∈ (f.pair g).range, x.2 * μ (⇑(f.pair g) ⁻¹' {x})

Tactic:
rw [Finset.sum_add_distrib]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x ∈ (f.pair g).range, x.1 * μ (⇑(f.pair g) ⁻¹' {x}) + ∑ x ∈ (f.pair g).range, x.2 * μ (⇑(f.pair g) ⁻¹' {x}) =
    (map Prod.fst (f.pair g)).lintegral μ + (map Prod.snd (f.pair g)).lintegral μ

Tactic:
rw [map_lintegral, map_lintegral]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ (f + g).lintegral μ = ∑ x ∈ (f.pair g).range, (x.1 * μ (⇑(f.pair g) ⁻¹' {x}) + x.2 * μ (⇑(f.pair g) ⁻¹' {x}))

Tactic:
rw [add_eq_map₂, map_lintegral]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x ∈ (f.pair g).range, (x.1 + x.2) * μ (⇑(f.pair g) ⁻¹' {x}) =
    ∑ x ∈ (f.pair g).range, (x.1 * μ (⇑(f.pair g) ⁻¹' {x}) + x.2 * μ (⇑(f.pair g) ⁻¹' {x}))

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x ∈ (f.pair g).range, (x.1 + x.2) * μ (⇑(f.pair g) ⁻¹' {x}) =
    ∑ x ∈ (f.pair g).range, (x.1 * μ (⇑(f.pair g) ⁻¹' {x}) + x.2 * μ (⇑(f.pair g) ⁻¹' {x}))

Tactic:
exact Finset.sum_congr rfl fun a _ => add_mul _ _ _

Result:
no goals
-- Mathlib/Probability/Moments/MGFAnalytic.lean
/-- For `t ∈ interior (integrableExpSet X μ)`, the derivative of `mgf X μ` at `t` is
`μ[X * exp (t * X)]`. -/
lemma hasDerivAt_mgf (h : t ∈ interior (integrableExpSet X μ)) :
    HasDerivAt (mgf X μ) (μ[fun ω ↦ X ω * exp (t * X ω)]) t

Proof state:
case h.e'_9.h.e'_7.h.h.e.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
x✝¹ x✝ : Ω
⊢ X x✝ = X x✝ ^ (0 + 1)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_8.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
x✝ : ℝ
⊢ mgf X μ x✝ = ∫ (x : Ω), (fun ω => X ω ^ 0 * rexp (x✝ * X ω)) x ∂μ

Tactic:
simp [mgf]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (mgf X μ) (∫ (x : Ω), (fun ω => X ω * rexp (t * X ω)) x ∂μ) t

Tactic:
convert hasDerivAt_integral_pow_mul_exp_real h 0

Result:
case h.e'_8.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
x✝ : ℝ
⊢ mgf X μ x✝ = ∫ (x : Ω), (fun ω => X ω ^ 0 * rexp (x✝ * X ω)) x ∂μ

case h.e'_9.h.e'_7.h.h.e.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
x✝¹ x✝ : Ω
⊢ X x✝ = X x✝ ^ (0 + 1)
-- Mathlib/LinearAlgebra/Ray.lean
theorem eq_zero_of_sameRay_neg_smul_right [NoZeroSMulDivisors R M] {r : R} (hr : r < 0)
    (h : SameRay R x (r • x)) : x = 0

Proof state:
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ r₂ * r < r₁

Tactic:
exact (mul_neg_of_pos_of_neg hr₂ hr).trans hr₁

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ x = 0

Tactic:
refine h.resolve_left (ne_of_gt <| sub_pos.2 ?_)

Result:
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ r₂ * r < r₁

Proof state:
case inr.inl
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
h₀ : r • x = 0
⊢ x = 0

Tactic:
simpa [hr.ne] using h₀

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
h : SameRay R x (r • x)
⊢ x = 0

Tactic:
rcases h with (rfl | h₀ | ⟨r₁, r₂, hr₁, hr₂, h⟩)

Result:
case inl
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
⊢ 0 = 0

case inr.inl
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
h₀ : r • x = 0
⊢ x = 0

case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • r • x
⊢ x = 0

Proof state:
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • r • x
⊢ x = 0

Tactic:
rw [← sub_eq_zero, smul_smul, ← sub_smul, smul_eq_zero] at h

Result:
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ x = 0
-- Mathlib/Algebra/Group/Basic.lean
theorem zpow_eq_zpow_emod' {x : G} (m : ℤ) {n : ℕ} (h : x ^ n = 1) :
    x ^ m = x ^ (m % (n : ℤ)) := zpow_eq_zpow_emod m (by simpa)

Proof state:
G : Type u_3
inst✝ : Group G
x : G
m : ℤ
n : ℕ
h : x ^ n = 1
⊢ x ^ ↑n = 1

Tactic:
simpa

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
@[simp]
lemma finrank_rootSpan_map_polarization_eq_finrank_corootSpan :
    finrank R (P.rootSpan.map P.Polarization) = finrank R P.corootSpan

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R N
h_ne : ∏ i : ι, (P.RootForm (P.root i)) (P.root i) ≠ 0
⊢ finrank R ↥P.corootSpan ≤ finrank R ↥(LinearMap.range (P.Polarization.domRestrict P.rootSpan))

Tactic:
refine LinearMap.finrank_le_of_isSMulRegular P.corootSpan
  (LinearMap.range (P.Polarization.domRestrict P.rootSpan))
  (smul_right_injective N h_ne)
  fun _ hx => ?_

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R N
h_ne : ∏ i : ι, (P.RootForm (P.root i)) (P.root i) ≠ 0
x✝ : N
hx : x✝ ∈ P.corootSpan
⊢ (∏ i : ι, (P.RootForm (P.root i)) (P.root i)) • x✝ ∈ LinearMap.range (P.Polarization.domRestrict P.rootSpan)
-- Mathlib/Analysis/Normed/Group/AddTorsor.lean
theorem edist_vadd_vadd_le (v v' : V) (p p' : P) :
    edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p'

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v v' : V
p p' : P
⊢ edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p'

Tactic:
simp only [edist_nndist]

Result:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v v' : V
p p' : P
⊢ ↑(nndist (v +ᵥ p) (v' +ᵥ p')) ≤ ↑(nndist v v') + ↑(nndist p p')

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v v' : V
p p' : P
⊢ ↑(nndist (v +ᵥ p) (v' +ᵥ p')) ≤ ↑(nndist v v') + ↑(nndist p p')

Tactic:
norm_cast

Result:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v v' : V
p p' : P
⊢ nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p'

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v v' : V
p p' : P
⊢ nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p'

Tactic:
apply dist_vadd_vadd_le

Result:
no goals
-- Mathlib/Probability/Martingale/Convergence.lean
theorem Integrable.tendsto_ae_condExp (hg : Integrable g μ)
    (hgmeas : StronglyMeasurable[⨆ n, ℱ n] g) :
    ∀ᵐ x ∂μ, Tendsto (fun n => (μ[g|ℱ n]) x) atTop (𝓝 (g x))

Proof state:
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
x✝ : μ s < ⊤
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
⊢ ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ

Tactic:
induction s, hs
  using MeasurableSpace.induction_on_inter (MeasurableSpace.measurableSpace_iSup_eq ℱ) hpi with
| empty =>
  simp only [measure_empty, Measure.restrict_empty, integral_zero_measure]
| basic s hs =>
  rcases hs with ⟨n, hn⟩
  exact this n _ hn
| compl t htmeas ht =>
  have hgeq := @setIntegral_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas (hg.trim hle hgmeas)
  have hheq := @setIntegral_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas
    (hlimint.trim hle stronglyMeasurable_limitProcess)
  rw [setIntegral_trim hle hgmeas htmeas.compl,
    setIntegral_trim hle stronglyMeasurable_limitProcess htmeas.compl, hgeq, hheq, ←
    setIntegral_trim hle hgmeas htmeas, ←
    setIntegral_trim hle stronglyMeasurable_limitProcess htmeas, ← integral_trim hle hgmeas, ←
    integral_trim hle stronglyMeasurable_limitProcess, ← setIntegral_univ,
    this 0 _ MeasurableSet.univ, setIntegral_univ, ht (measure_lt_top _ _)]
| iUnion f hf hfmeas heq =>
  rw [integral_iUnion (fun n => hle _ (hfmeas n)) hf hg.integrableOn,
    integral_iUnion (fun n => hle _ (hfmeas n)) hf hlimint.integrableOn]
  exact tsum_congr fun n => heq _ (measure_lt_top _ _)

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem toCycle_eq_toList (f : Perm α) (hf : IsCycle f) (x : α) (hx : f x ≠ x) :
    toCycle f hf = toList f x

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
key : Finset.univ.val = x ::ₘ Finset.univ.val.erase x
⊢ (x ::ₘ Finset.univ.val.erase x).recOn (Quot.mk ⇑(IsRotated.setoid α) [])
      (fun x x_1 l => if f x = x then l else ↑(f.toList x)) ⋯ =
    ↑(f.toList x)

Tactic:
simp [hx]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
key : Finset.univ.val = x ::ₘ Finset.univ.val.erase x
⊢ f.toCycle hf = ↑(f.toList x)

Tactic:
rw [toCycle, key]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
key : Finset.univ.val = x ::ₘ Finset.univ.val.erase x
⊢ (x ::ₘ Finset.univ.val.erase x).recOn (Quot.mk ⇑(IsRotated.setoid α) [])
      (fun x x_1 l => if f x = x then l else ↑(f.toList x)) ⋯ =
    ↑(f.toList x)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
⊢ Finset.univ.val = x ::ₘ Finset.univ.val.erase x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
⊢ f.toCycle hf = ↑(f.toList x)

Tactic:
have key : (Finset.univ : Finset α).val = x ::ₘ Finset.univ.val.erase x := by simp

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
key : Finset.univ.val = x ::ₘ Finset.univ.val.erase x
⊢ f.toCycle hf = ↑(f.toList x)