harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Nat.pow_imp_self_of_one_lt {M} [Monoid M] (k : ℕ) (hk : 1 < k)
    (P : M → Prop) (hmul : ∀ x y, P x → P (x * y) ∨ P (y * x))
    (hpow : ∀ x, P (x ^ k) → P x) : ∀ n x, P (x ^ n) → P x :=
  k.cauchy_induction_mul (fun n ih x hx ↦ ih x <| (hmul _ x hx).elim
    (fun h ↦ by rwa [_root_.pow_succ]) fun h ↦ by rwa [_root_.pow_succ']) 0 hk
    (fun x hx ↦ pow_one x ▸ hx) fun n _ hn x hx ↦ hpow x <| hn _ <| (pow_mul x k n).subst hx

Proof state:
M : Type u_1
inst✝ : Monoid M
k : ℕ
hk : 1 < k
P : M → Prop
hmul : ∀ (x y : M), P x → P (x * y) ∨ P (y * x)
hpow : ∀ (x : M), P (x ^ k) → P x
n : ℕ
ih : ∀ (x : M), P (x ^ (n + 1)) → P x
x : M
hx : P (x ^ n)
h : P (x ^ n * x)
⊢ P (x ^ (n + 1))

Tactic:
rwa [_root_.pow_succ]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
k : ℕ
hk : 1 < k
P : M → Prop
hmul : ∀ (x y : M), P x → P (x * y) ∨ P (y * x)
hpow : ∀ (x : M), P (x ^ k) → P x
n : ℕ
ih : ∀ (x : M), P (x ^ (n + 1)) → P x
x : M
hx : P (x ^ n)
h : P (x * x ^ n)
⊢ P (x ^ (n + 1))

Tactic:
rwa [_root_.pow_succ']

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
lemma strictAntiOn_of_add_one_lt (hs : s.OrdConnected) :
    (∀ a, ¬ IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) < f a) → StrictAntiOn f s

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) < f a) → StrictAntiOn f s

Tactic:
simpa [Order.succ_eq_add_one] using strictAntiOn_of_succ_lt hs (f := f)

Result:
no goals
-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma restrict_restrict_hom (f : X.PartialMap Y)
    (U : X.Opens) (hU : Dense (U : Set X)) (hU' : U ≤ f.domain)
    (V : X.Opens) (hV : Dense (V : Set X)) (hV' : V ≤ U) :
    ((f.restrict U hU hU').restrict V hV hV').hom = (f.restrict V hV (hV'.trans hU')).hom

Proof state:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
V : X.Opens
hV : Dense ↑V
hV' : V ≤ U
⊢ ((f.restrict U hU hU').restrict V hV hV').hom = (f.restrict V hV ⋯).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem nhdsWithin_isUnit_neBot : NeBot (𝓝[{ x : α | IsUnit x }] 0)

Proof state:
α : Type u_2
inst✝ : NontriviallyNormedField α
⊢ (𝓝[{x | IsUnit x}] 0).NeBot

Tactic:
simpa only [isUnit_iff_ne_zero] using punctured_nhds_neBot (0 : α)

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem coe_int_add_eq_mod {n : Nat} (u v : Fin n) :
    ((u + v : Fin n) : Int) = ((u : Int) + (v : Int)) % n

Proof state:
n : ℕ
u v : Fin n
⊢ ↑↑(u + v) = (↑↑u + ↑↑v) % ↑n

Tactic:
rw [coe_int_add_eq_ite]

Result:
n : ℕ
u v : Fin n
⊢ (if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n) = (↑↑u + ↑↑v) % ↑n

Proof state:
case isTrue
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑↑u + ↑↑v = (↑↑u + ↑↑v) % ↑n

Tactic:
rw [Int.emod_eq_of_lt] <;> omega

Result:
no goals

Proof state:
n : ℕ
u v : Fin n
⊢ (if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n) = (↑↑u + ↑↑v) % ↑n

Tactic:
split

Result:
case isTrue
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑↑u + ↑↑v = (↑↑u + ↑↑v) % ↑n

case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑↑u + ↑↑v - ↑n = (↑↑u + ↑↑v) % ↑n

Proof state:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑↑u + ↑↑v - ↑n = (↑↑u + ↑↑v) % ↑n

Tactic:
rw [Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt] <;> omega

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem oangle_rotation_self_left {x : V} (hx : x ≠ 0) (θ : Real.Angle) :
    o.oangle (o.rotation θ x) x = -θ

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ o.oangle ((o.rotation θ) x) x = -θ

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem empty_iff {s : Ordset α} : s = ∅ ↔ s.1.empty :=
  ⟨fun h => by cases h; exact rfl,
    fun h => by cases s with | mk s_val _ => cases s_val <;> [rfl; cases h]⟩

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Ordset α
h : (↑s).empty = true
⊢ s = ∅

Tactic:
cases s with | mk s_val _ => cases s_val <;> [rfl; cases h]

Result:
no goals

Proof state:
case refl
α : Type u_1
inst✝ : Preorder α
⊢ (↑∅).empty = true

Tactic:
exact rfl

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝ : Preorder α
s_val : Ordnode α
property✝ : s_val.Valid
h : (↑⟨s_val, property✝⟩).empty = true
⊢ ⟨s_val, property✝⟩ = ∅

Tactic:
cases s_val <;> [rfl; cases h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Ordset α
h : s = ∅
⊢ (↑s).empty = true

Tactic:
cases h

Result:
case refl
α : Type u_1
inst✝ : Preorder α
⊢ (↑∅).empty = true
-- Mathlib/Data/List/SplitLengths.lean
theorem flatten_splitLengths (h : l.length ≤ sz.sum) : (sz.splitLengths l).flatten = l

Proof state:
case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), l.length ≤ tail✝.sum → (tail✝.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head✝ :: tail✝).sum
⊢ ((head✝ :: tail✝).splitLengths l).flatten = l

Tactic:
case cons head tail ih =>
  simp only [splitLengths_cons, flatten_cons]
  rw [ih, take_append_drop]
  simpa [add_comm] using h

Result:
no goals

Proof state:
case nil
α : Type u_1
l : List α
h : l.length ≤ [].sum
⊢ ([].splitLengths l).flatten = l

Tactic:
simp_all

Result:
no goals

Proof state:
case h
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ (drop head l).length ≤ tail.sum

Tactic:
simpa [add_comm] using h

Result:
no goals

Proof state:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ take head l ++ (tail.splitLengths (drop head l)).flatten = l

Tactic:
rw [ih, take_append_drop]

Result:
case h
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ (drop head l).length ≤ tail.sum

Proof state:
α : Type u_1
l : List α
sz : List ℕ
h : l.length ≤ sz.sum
⊢ (sz.splitLengths l).flatten = l

Tactic:
induction sz generalizing l

Result:
case nil
α : Type u_1
l : List α
h : l.length ≤ [].sum
⊢ ([].splitLengths l).flatten = l

case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), l.length ≤ tail✝.sum → (tail✝.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head✝ :: tail✝).sum
⊢ ((head✝ :: tail✝).splitLengths l).flatten = l

Proof state:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ ((head :: tail).splitLengths l).flatten = l

Tactic:
simp only [splitLengths_cons, flatten_cons]

Result:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ take head l ++ (tail.splitLengths (drop head l)).flatten = l
-- Mathlib/Analysis/Complex/Hadamard.lean
/-- `sSup` of `norm` translated by `ε > 0` is positive applied to the image of `f` on the
vertical line `re z = x` -/
lemma sSupNormIm_eps_pos {ε : ℝ} (hε : ε > 0) (x : ℝ) : 0 < ε + sSupNormIm f x

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
x : ℝ
⊢ 0 < ε + sSupNormIm f x

Tactic:
linarith [sSupNormIm_nonneg f x]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem inv_divInt (n d : Int) : (n /. d).inv = d /. n

Proof state:
n d : Int
z : ¬d = 0
⊢ (n /. d).inv = d /. n

Tactic:
cases e : n /. d

Result:
case mk'
n d : Int
z : ¬d = 0
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
e : n /. d = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }.inv = d /. n

Proof state:
case mk'
n d : Int
z : ¬d = 0
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
e : n /. d = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }.inv = d /. n

Tactic:
rcases divInt_num_den z e with ⟨g, zg, rfl, rfl⟩

Result:
case mk'.intro.intro.intro
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
g : Int
zg : g ≠ 0
z : ¬↑den✝ * g = 0
e : num✝ * g /. (↑den✝ * g) = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }.inv = ↑den✝ * g /. (num✝ * g)

Proof state:
n d : Int
z : d = 0
⊢ (n /. d).inv = d /. n

Tactic:
simp [z]

Result:
no goals

Proof state:
case mk'.intro.intro.intro
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
g : Int
zg : g ≠ 0
z : ¬↑den✝ * g = 0
e : num✝ * g /. (↑den✝ * g) = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }.inv = ↑den✝ * g /. (num✝ * g)

Tactic:
simp [inv_def, divInt_mul_right zg]

Result:
no goals

Proof state:
n d : Int
⊢ (n /. d).inv = d /. n

Tactic:
if z : d = 0 then simp [z] else
cases e : n /. d; rcases divInt_num_den z e with ⟨g, zg, rfl, rfl⟩
simp [inv_def, divInt_mul_right zg]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem FactorSet.sup_add_inf_eq_add [DecidableEq (Associates α)] :
    ∀ a b : FactorSet α, a ⊔ b + a ⊓ b = a + b
  | ⊤, b => show ⊤ ⊔ b + ⊤ ⊓ b = ⊤ + b by simp
  | a, ⊤ => show a ⊔ ⊤ + a ⊓ ⊤ = a + ⊤ by simp
  | WithTop.some a, WithTop.some b =>
    show (a : FactorSet α) ⊔ b + (a : FactorSet α) ⊓ b = a + b by
      rw [← WithTop.coe_sup, ← WithTop.coe_inf, ← WithTop.coe_add, ← WithTop.coe_add,
        WithTop.coe_eq_coe]
      exact Multiset.union_add_inter _ _

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
b : FactorSet α
⊢ ⊤ ⊔ b + ⊤ ⊓ b = ⊤ + b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
a b : Multiset { a // Irreducible a }
⊢ ↑a ⊔ ↑b + ↑a ⊓ ↑b = ↑a + ↑b

Tactic:
rw [← WithTop.coe_sup, ← WithTop.coe_inf, ← WithTop.coe_add, ← WithTop.coe_add,
  WithTop.coe_eq_coe]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
a b : Multiset { a // Irreducible a }
⊢ a ⊔ b + a ⊓ b = a + b

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
a : FactorSet α
⊢ a ⊔ ⊤ + a ⊓ ⊤ = a + ⊤

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
a b : Multiset { a // Irreducible a }
⊢ a ⊔ b + a ⊓ b = a + b

Tactic:
exact Multiset.union_add_inter _ _

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp] protected lemma not_top_lt (a : WithTop α) : ¬⊤ < a

Proof state:
α : Type u_1
inst✝ : LT α
a : WithTop α
⊢ ¬⊤ < a

Tactic:
simp [lt_def]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
@[to_additive]
lemma isBlock_iff_disjoint_smul_of_ne :
    IsBlock G B ↔ ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
⊢ IsBlock G B ↔ ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B

Tactic:
refine ⟨fun hB g ↦ by simpa using hB (g₂ := 1), fun hB g₁ g₂ h ↦ ?_⟩

Result:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B
g₁ g₂ : G
h : g₁ • B ≠ g₂ • B
⊢ Disjoint (g₁ • B) (g₂ • B)

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
g : G
⊢ g • B ≠ B → Disjoint (g • B) B

Tactic:
simpa using hB (g₂ := 1)

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B
g₁ g₂ : G
h : g₁ • B ≠ g₂ • B
⊢ Disjoint (g₁ • B) (g₂ • B)

Tactic:
simp only [disjoint_smul_set_right, ne_eq, ← inv_smul_eq_iff, smul_smul] at h ⊢

Result:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B
g₁ g₂ : G
h : ¬(g₂⁻¹ * g₁) • B = B
⊢ Disjoint ((g₂⁻¹ * g₁) • B) B

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B
g₁ g₂ : G
h : ¬(g₂⁻¹ * g₁) • B = B
⊢ Disjoint ((g₂⁻¹ * g₁) • B) B

Tactic:
exact hB h

Result:
no goals
-- Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean
theorem _root_.IsLocalization.AtPrime.prime_unique_of_minimal {S} [CommSemiring S] [Algebra R S]
    [IsLocalization.AtPrime S I] {J K : Ideal S} [J.IsPrime] [K.IsPrime] : J = K :=
  haveI : Subsingleton {i : Ideal R // i.IsPrime ∧ i ≤ I} := ⟨fun i₁ i₂ ↦ Subtype.ext <| by
    rw [minimalPrimes_eq_minimals, Set.mem_setOf] at hMin
    rw [hMin.eq_of_le i₁.2.1 i₁.2.2, hMin.eq_of_le i₂.2.1 i₂.2.2]⟩
  Subtype.ext_iff.mp <| (IsLocalization.AtPrime.orderIsoOfPrime S I).injective
    (a₁ := ⟨J, ‹_›⟩) (a₂ := ⟨K, ‹_›⟩) (Subsingleton.elim _ _)

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
I : Ideal R
hI : I.IsPrime
hMin : Minimal Ideal.IsPrime I
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : IsLocalization.AtPrime S I
J K : Ideal S
inst✝¹ : J.IsPrime
inst✝ : K.IsPrime
i₁ i₂ : { i // i.IsPrime ∧ i ≤ I }
⊢ ↑i₁ = ↑i₂

Tactic:
rw [hMin.eq_of_le i₁.2.1 i₁.2.2, hMin.eq_of_le i₂.2.1 i₂.2.2]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
I : Ideal R
hI : I.IsPrime
hMin : I ∈ minimalPrimes R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : IsLocalization.AtPrime S I
J K : Ideal S
inst✝¹ : J.IsPrime
inst✝ : K.IsPrime
i₁ i₂ : { i // i.IsPrime ∧ i ≤ I }
⊢ ↑i₁ = ↑i₂

Tactic:
rw [minimalPrimes_eq_minimals, Set.mem_setOf] at hMin

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
I : Ideal R
hI : I.IsPrime
hMin : Minimal Ideal.IsPrime I
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : IsLocalization.AtPrime S I
J K : Ideal S
inst✝¹ : J.IsPrime
inst✝ : K.IsPrime
i₁ i₂ : { i // i.IsPrime ∧ i ≤ I }
⊢ ↑i₁ = ↑i₂
-- Mathlib/Topology/Semicontinuous.lean
theorem upperSemicontinuous_iff_isClosed_preimage {f : α → γ} :
    UpperSemicontinuous f ↔ ∀ y, IsClosed (f ⁻¹' Ici y)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_3
inst✝ : LinearOrder γ
f : α → γ
⊢ (∀ (y : γ), IsOpen (f ⁻¹' Iio y)) ↔ ∀ (y : γ), IsClosed (f ⁻¹' Ici y)

Tactic:
simp only [← isOpen_compl_iff, ← preimage_compl, compl_Ici]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_3
inst✝ : LinearOrder γ
f : α → γ
⊢ UpperSemicontinuous f ↔ ∀ (y : γ), IsClosed (f ⁻¹' Ici y)

Tactic:
rw [upperSemicontinuous_iff_isOpen_preimage]

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_3
inst✝ : LinearOrder γ
f : α → γ
⊢ (∀ (y : γ), IsOpen (f ⁻¹' Iio y)) ↔ ∀ (y : γ), IsClosed (f ⁻¹' Ici y)
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma inv_zero : (0 : EReal)⁻¹ = 0

Proof state:
⊢ ↑0⁻¹ = 0

Tactic:
rw [GroupWithZero.inv_zero, coe_zero]

Result:
no goals

Proof state:
⊢ 0⁻¹ = 0

Tactic:
change (0 : ℝ)⁻¹ = (0 : EReal)

Result:
⊢ ↑0⁻¹ = 0
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_eq_left {a b : Cardinal} (ha : ℵ₀ ≤ a) (hb : b ≤ a) (hb' : b ≠ 0) : a * b = a

Proof state:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
hb' : b ≠ 0
⊢ a * b = a

Tactic:
rw [mul_eq_max_of_aleph0_le_left ha hb', max_eq_left hb]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem smul_measure (c : ℝ≥0∞) (hc_ne_zero : c ≠ 0) (hT : FinMeasAdditive μ T) :
    FinMeasAdditive (c • μ) T

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : μ s = ⊤
⊢ μ s = ⊤ ∨ c = ⊤ ∧ ¬μ s = 0

Tactic:
exact Or.inl hμs

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : μ s = ⊤
⊢ c ≠ 0 ∧ μ s = ⊤ ∨ c = ⊤ ∧ μ s ≠ 0

Tactic:
simp only [hc_ne_zero, true_and, Ne, not_false_iff]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : μ s = ⊤
⊢ μ s = ⊤ ∨ c = ⊤ ∧ ¬μ s = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : μ s = ⊤
⊢ (c • μ) s = ⊤

Tactic:
rw [Measure.smul_apply, smul_eq_mul, ENNReal.mul_eq_top]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : μ s = ⊤
⊢ c ≠ 0 ∧ μ s = ⊤ ∨ c = ⊤ ∧ μ s ≠ 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
⊢ FinMeasAdditive (c • μ) T

Tactic:
refine of_eq_top_imp_eq_top (fun s _ hμs => ?_) hT

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : μ s = ⊤
⊢ (c • μ) s = ⊤
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem iSup_mul_nat (o : Ordinal) : ⨆ n : ℕ, o * n = o * ω

Proof state:
case inl

⊢ ⨆ n, 0 * ↑n = 0

Tactic:
exact iSup_eq_zero_iff.2 fun n => zero_mul (n : Ordinal)

Result:
no goals

Proof state:
o : Ordinal.{u_1}
⊢ ⨆ n, o * ↑n = o * ω

Tactic:
rcases eq_zero_or_pos o with (rfl | ho)

Result:
case inl

⊢ ⨆ n, 0 * ↑n = 0 * ω

case inr
o : Ordinal.{u_1}
ho : 0 < o
⊢ ⨆ n, o * ↑n = o * ω

Proof state:
case inr
o : Ordinal.{u_1}
ho : 0 < o
⊢ ⨆ n, o * ↑n = o * ω

Tactic:
exact (isNormal_mul_right ho).apply_omega0

Result:
no goals

Proof state:
case inl

⊢ ⨆ n, 0 * ↑n = 0 * ω

Tactic:
rw [zero_mul]

Result:
case inl

⊢ ⨆ n, 0 * ↑n = 0
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem seq_apply : (seq q p) b = ∑' (f : α → β) (a : α), if b = f a then q f * p a else 0

Proof state:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
⊢ (q.seq p) b = ∑' (f : α → β) (a : α), if b = f a then q f * p a else 0

Tactic:
simp only [seq, mul_boole, bind_apply, pure_apply]

Result:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
⊢ (∑' (a : α → β), q a * ∑' (a_1 : α), if b = a a_1 then p a_1 else 0) =
    ∑' (f : α → β) (a : α), if b = f a then q f * p a else 0

Proof state:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
⊢ (∑' (a : α → β), q a * ∑' (a_1 : α), if b = a a_1 then p a_1 else 0) =
    ∑' (f : α → β) (a : α), if b = f a then q f * p a else 0

Tactic:
refine tsum_congr fun f => ENNReal.tsum_mul_left.symm.trans (tsum_congr fun a => ?_)

Result:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
f : α → β
a : α
⊢ (q f * if b = f a then p a else 0) = if b = f a then q f * p a else 0

Proof state:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
f : α → β
a : α
⊢ (q f * if b = f a then p a else 0) = if b = f a then q f * p a else 0

Tactic:
simpa only [mul_zero] using mul_ite (b = f a) (q f) (p a) 0

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_flatMap_eq_none_iff {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
    (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y

Proof state:
α : Type u_1
n : Nat
β : Type
m : Nat
xs : Vector α n
f : α → Vector β m
p : β → Bool
⊢ find? p (xs.flatMap f) = none ↔ ∀ (x : α), x ∈ xs → ∀ (y : β), y ∈ f x → (!p y) = true

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b = 1 :=
  eq_one_of_mul_eq_one_right (b := a) H <| by rw [Int.mul_comm, H']

Proof state:
a b : Int
H : 0 ≤ b
H' : a * b = 1
⊢ b * a = 1

Tactic:
rw [Int.mul_comm, H']

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem lt_base_pow_length_digits' {b m : ℕ} : m < (b + 2) ^ (digits (b + 2) m).length

Proof state:
case h.e'_3
b m : ℕ
⊢ m = ofDigits (b + 2) ((b + 2).digits m)

Tactic:
rw [ofDigits_digits (b + 2) m]

Result:
no goals

Proof state:
b m : ℕ
⊢ m < (b + 2) ^ ((b + 2).digits m).length

Tactic:
convert @ofDigits_lt_base_pow_length' b (digits (b + 2) m) fun _ => digits_lt_base'

Result:
case h.e'_3
b m : ℕ
⊢ m = ofDigits (b + 2) ((b + 2).digits m)
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_eq_det_toMatrix_of_finset [DecidableEq M] {s : Finset M} (b : Basis s A M)
    (f : M →ₗ[A] M) : LinearMap.det f = Matrix.det (LinearMap.toMatrix b b f)

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
s : Finset M
b : Basis { x // x ∈ s } A M
f : M →ₗ[A] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ LinearMap.det f = ((toMatrix b b) f).det

Tactic:
rw [LinearMap.coe_det, dif_pos, detAux_def'' _ b] <;> assumption

Result:
no goals

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
s : Finset M
b : Basis { x // x ∈ s } A M
f : M →ₗ[A] M
⊢ LinearMap.det f = ((toMatrix b b) f).det

Tactic:
have : ∃ s : Finset M, Nonempty (Basis s A M) := ⟨s, ⟨b⟩⟩

Result:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
s : Finset M
b : Basis { x // x ∈ s } A M
f : M →ₗ[A] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ LinearMap.det f = ((toMatrix b b) f).det
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
    (h := getElem_extract_loop_lt_aux as bs size start hlt) :
    (extract.loop as size start bs)[i] = bs[i]

Proof state:
case e_xs
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hlt : i < bs.size
h : optParam (i < (extract.loop as size start bs).size) ⋯
⊢ extract.loop as size start bs = bs ++ extract.loop as size start #[]

Tactic:
rw [extract_loop_eq_aux]

Result:
no goals

Proof state:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hlt : i < bs.size
h : optParam (i < (extract.loop as size start bs).size) ⋯
⊢ i < (bs ++ extract.loop as size start #[]).size

Tactic:
rw [size_append]

Result:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hlt : i < bs.size
h : optParam (i < (extract.loop as size start bs).size) ⋯
⊢ i < bs.size + (extract.loop as size start #[]).size

Proof state:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hlt : i < bs.size
h : optParam (i < (extract.loop as size start bs).size) ⋯
⊢ i < bs.size + (extract.loop as size start #[]).size

Tactic:
exact Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)

Result:
no goals

Proof state:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hlt : i < bs.size
h : optParam (i < (extract.loop as size start bs).size) ⋯
⊢ (extract.loop as size start bs)[i] = (bs ++ extract.loop as size start #[])[i]

Tactic:
congr

Result:
case e_xs
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hlt : i < bs.size
h : optParam (i < (extract.loop as size start bs).size) ⋯
⊢ extract.loop as size start bs = bs ++ extract.loop as size start #[]

Proof state:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hlt : i < bs.size
h : optParam (i < (extract.loop as size start bs).size) ⋯
⊢ (extract.loop as size start bs)[i] = bs[i]

Tactic:
apply Eq.trans _ (getElem_append_left (bs:=extract.loop as size start #[]) hlt)

Result:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hlt : i < bs.size
h : optParam (i < (extract.loop as size start bs).size) ⋯
⊢ i < (bs ++ extract.loop as size start #[]).size

α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hlt : i < bs.size
h : optParam (i < (extract.loop as size start bs).size) ⋯
⊢ (extract.loop as size start bs)[i] = (bs ++ extract.loop as size start #[])[i]