harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Constructions/Projective.lean
theorem unique [∀ i, IsFiniteMeasure (P i)]
    (hμ : IsProjectiveLimit μ P) (hν : IsProjectiveLimit ν P) :
    μ = ν

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ ν : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
⊢ μ = ν

Tactic:
haveI : IsFiniteMeasure μ := hμ.isFiniteMeasure

Result:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ ν : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
this : IsFiniteMeasure μ
⊢ μ = ν

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ ν : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
this : IsFiniteMeasure μ
s : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
⊢ μ s = ν s

Tactic:
obtain ⟨I, S, hS, rfl⟩ := (mem_measurableCylinders _).mp hs

Result:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ ν : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
this : IsFiniteMeasure μ
I : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders α
⊢ μ (cylinder I S) = ν (cylinder I S)

Proof state:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ ν : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
this : IsFiniteMeasure μ
I : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders α
⊢ μ (cylinder I S) = ν (cylinder I S)

Tactic:
rw [hμ.measure_cylinder _ hS, hν.measure_cylinder _ hS]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ ν : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
this : IsFiniteMeasure μ
⊢ μ = ν

Tactic:
refine ext_of_generate_finite (measurableCylinders α) generateFrom_measurableCylinders.symm
  isPiSystem_measurableCylinders (fun s hs ↦ ?_) (hμ.measure_univ_unique hν)

Result:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ ν : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
this : IsFiniteMeasure μ
s : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
⊢ μ s = ν s
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem map_iInf_of_ker_le {f : F} (hf : Surjective f) {ι} {p : ι → Submodule R M}
    (h : LinearMap.ker f ≤ ⨅ i, p i) : map f (⨅ i, p i) = ⨅ i, map f (p i)

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_8
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
hf : Surjective ⇑f
ι : Sort u_9
p : ι → Submodule R M
h : LinearMap.ker f ≤ ⨅ i, p i
⊢ map f (⨅ i, p i) = map f (⨅ i, comap f (map f (p i)))

Tactic:
simp_rw [fun i ↦ comap_map_eq_self (le_iInf_iff.mp h i)]

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_8
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
hf : Surjective ⇑f
ι : Sort u_9
p : ι → Submodule R M
h : LinearMap.ker f ≤ ⨅ i, p i
⊢ map f (⨅ i, p i) = ⨅ i, map f (p i)

Tactic:
conv_rhs => rw [← map_comap_eq_of_surjective hf (⨅ _, _), comap_iInf]

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_8
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
hf : Surjective ⇑f
ι : Sort u_9
p : ι → Submodule R M
h : LinearMap.ker f ≤ ⨅ i, p i
⊢ map f (⨅ i, p i) = map f (⨅ i, comap f (map f (p i)))
-- Mathlib/Topology/DenseEmbedding.lean
theorem isClosed_property [TopologicalSpace β] {e : α → β} {p : β → Prop} (he : DenseRange e)
    (hp : IsClosed { x | p x }) (h : ∀ a, p (e a)) : ∀ b, p b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
e : α → β
p : β → Prop
he : DenseRange e
hp : IsClosed {x | p x}
h : ∀ (a : α), p (e a)
this : univ ⊆ {b | p b}
⊢ ∀ (b : β), p b

Tactic:
simpa only [univ_subset_iff, eq_univ_iff_forall, mem_setOf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
e : α → β
p : β → Prop
he : DenseRange e
hp : IsClosed {x | p x}
h : ∀ (a : α), p (e a)
⊢ ∀ (b : β), p b

Tactic:
have : univ ⊆ { b | p b } :=
  calc
    univ = closure (range e) := he.closure_range.symm
    _ ⊆ closure { b | p b } := closure_mono <| range_subset_iff.mpr h
    _ = _ := hp.closure_eq

Result:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
e : α → β
p : β → Prop
he : DenseRange e
hp : IsClosed {x | p x}
h : ∀ (a : α), p (e a)
this : univ ⊆ {b | p b}
⊢ ∀ (b : β), p b
-- Mathlib/Logic/Basic.lean
theorem mem_dite {a : α} {s : p → β} {t : ¬p → β} :
    (a ∈ if h : p then s h else t h) ↔ (∀ h, a ∈ s h) ∧ (∀ h, a ∈ t h)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : α
s : p → β
t : ¬p → β
⊢ (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h

Tactic:
by_cases h : p <;> simp [h]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem nonneg_mul_lem {x y : ℕ} {a : ℤ√d} (ha : Nonneg a) : Nonneg (⟨x, y⟩ * a)

Proof state:
d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
⊢ ({ re := ↑x, im := ↑y } * a).Nonneg

Tactic:
have : (⟨x, y⟩ * a : ℤ√d) = (x : ℤ√d) * a + sqrtd * ((y : ℤ√d) * a) := by
  rw [decompose, right_distrib, mul_assoc, Int.cast_natCast, Int.cast_natCast]

Result:
d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ ({ re := ↑x, im := ↑y } * a).Nonneg

Proof state:
d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ (↑x * a + sqrtd * (↑y * a)).Nonneg

Tactic:
exact (nonneg_smul ha).add (nonneg_muld <| nonneg_smul ha)

Result:
no goals

Proof state:
d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ ({ re := ↑x, im := ↑y } * a).Nonneg

Tactic:
rw [this]

Result:
d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ (↑x * a + sqrtd * (↑y * a)).Nonneg

Proof state:
d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
⊢ { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)

Tactic:
rw [decompose, right_distrib, mul_assoc, Int.cast_natCast, Int.cast_natCast]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_lf_zero_iff {x : PGame} : -x ⧏ 0 ↔ 0 ⧏ x

Proof state:
x : PGame
⊢ -x ⧏ 0 ↔ 0 ⧏ x

Tactic:
rw [neg_lf_iff, neg_zero]

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem multichoose_neg_of_lt (n k : ℕ) (h : n < k) : multichoose (-n : ℤ) k = 0

Proof state:
n k : ℕ
h : n < k
⊢ multichoose (-↑n) k = 0

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero k),
  factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_neg_of_lt h, smul_zero]

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem zpow_y_lt_iff_lt {a : Solution₁ d} (h : IsFundamental a) (m n : ℤ) :
    (a ^ m).y < (a ^ n).y ↔ m < n

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
H : (a ^ m).y < (a ^ n).y
⊢ m < n

Tactic:
contrapose! H

Result:
d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
H : n ≤ m
⊢ (a ^ n).y ≤ (a ^ m).y

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
⊢ (a ^ m).y < (a ^ n).y ↔ m < n

Tactic:
refine ⟨fun H => ?_, fun H => h.y_strictMono H⟩

Result:
d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
H : (a ^ m).y < (a ^ n).y
⊢ m < n

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
H : n ≤ m
⊢ (a ^ n).y ≤ (a ^ m).y

Tactic:
exact h.y_strictMono.monotone H

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/Classification.lean
theorem cardinal_le_max_transcendence_basis (hv : IsTranscendenceBasis R v) :
    Cardinal.lift.{max u w} #K ≤ max (max (Cardinal.lift.{max v w} #R)
      (Cardinal.lift.{max u v} #ι)) ℵ₀ :=
  calc
    Cardinal.lift.{max u w} #K ≤ Cardinal.lift.{max u w}
        (max #(Algebra.adjoin R (Set.range v)) ℵ₀)

Proof state:
R : Type u
K : Type v
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type w
v : ι → K
hv : IsTranscendenceBasis R v
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
⊢ Cardinal.lift.{max u w, v} #K ≤ Cardinal.lift.{max u w, v} (#↥(Algebra.adjoin R (Set.range v)) ⊔ ℵ₀)

Tactic:
simpa using Algebra.IsAlgebraic.cardinalMk_le_max (Algebra.adjoin R (Set.range v)) K

Result:
no goals

Proof state:
R : Type u
K : Type v
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type w
v : ι → K
hv : IsTranscendenceBasis R v
⊢ Cardinal.lift.{v, max u w} (Cardinal.lift.{w, u} #R ⊔ Cardinal.lift.{u, w} #ι ⊔ ℵ₀ ⊔ ℵ₀) =
    Cardinal.lift.{max v w, u} #R ⊔ Cardinal.lift.{max u v, w} #ι ⊔ ℵ₀

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
K : Type v
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type w
v : ι → K
hv : IsTranscendenceBasis R v
⊢ Cardinal.lift.{max u w, v} #K ≤ Cardinal.lift.{max u w, v} (#↥(Algebra.adjoin R (Set.range v)) ⊔ ℵ₀)

Tactic:
letI := isAlgClosure_of_transcendence_basis v hv

Result:
R : Type u
K : Type v
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type w
v : ι → K
hv : IsTranscendenceBasis R v
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
⊢ Cardinal.lift.{max u w, v} #K ≤ Cardinal.lift.{max u w, v} (#↥(Algebra.adjoin R (Set.range v)) ⊔ ℵ₀)

Proof state:
R : Type u
K : Type v
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type w
v : ι → K
hv : IsTranscendenceBasis R v
⊢ Cardinal.lift.{max u w, v} (#↥(Algebra.adjoin R (Set.range v)) ⊔ ℵ₀) =
    Cardinal.lift.{v, max u w} (#(MvPolynomial ι R) ⊔ ℵ₀)

Tactic:
rw [lift_max, ← Cardinal.lift_mk_eq.2 ⟨hv.1.aevalEquiv.toEquiv⟩, lift_aleph0,
  ← lift_aleph0.{max u v w, max u w}, ← lift_max, lift_umax.{max u w, v}]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertMany_list_singleton {k : α} {v : β} :
    insertMany m [⟨k, v⟩] = m.insert k v

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw₀ α fun x => β
k : α
v : β
⊢ (insertMany m [(k, v)]).val = m.insert k v

Tactic:
simp [insertMany, Id.run]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_succ [AddMonoidWithOne α] (n : PosNum) : (succ n : α) = n + 1

Proof state:
α : Type u_1
inst✝ : AddMonoidWithOne α
n : PosNum
⊢ ↑n.succ = ↑n + 1

Tactic:
rw [← add_one, cast_add, cast_one]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem divBy_mul_by (s : S) (p : LocalizedModule S M) :
    divBy s (algebraMap R (Module.End R (LocalizedModule S M)) s p) = p :=
  p.induction_on fun m t => by
    rw [Module.algebraMap_end_apply, divBy_apply]
    erw [smul_def]
    rw [LocalizedModule.liftOn_mk, mul_assoc, ← smul_def]
    erw [smul'_mk]
    rw [← Submonoid.smul_def, mk_cancel_common_right _ s]

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ mk (↑s • m) (t * s) = mk m t

Tactic:
rw [← Submonoid.smul_def, mk_cancel_common_right _ s]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ (mk ((IsLocalization.sec S (↑(algebraMap R (Localization S)).toMonoidWithZeroHom ↑s)).1 • m)
          ((IsLocalization.sec S (↑(algebraMap R (Localization S)).toMonoidWithZeroHom ↑s)).2 * t)).liftOn
      (fun p => mk p.1 (p.2 * s)) ⋯ =
    mk m t

Tactic:
rw [LocalizedModule.liftOn_mk, mul_assoc, ← smul_def]

Result:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ ↑(algebraMap R (Localization S)).toMonoidWithZeroHom ↑s • mk m (t * s) = mk m t

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ (divBy s) (((algebraMap R (Module.End R (LocalizedModule S M))) ↑s) (mk m t)) = mk m t

Tactic:
rw [Module.algebraMap_end_apply, divBy_apply]

Result:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ (↑s • mk m t).liftOn (fun p => mk p.1 (p.2 * s)) ⋯ = mk m t

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ ↑(algebraMap R (Localization S)).toMonoidWithZeroHom ↑s • mk m (t * s) = mk m t

Tactic:
erw [smul'_mk]

Result:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ mk (↑s • m) (t * s) = mk m t

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ (↑s • mk m t).liftOn (fun p => mk p.1 (p.2 * s)) ⋯ = mk m t

Tactic:
erw [smul_def]

Result:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ (mk ((IsLocalization.sec S (↑(algebraMap R (Localization S)).toMonoidWithZeroHom ↑s)).1 • m)
          ((IsLocalization.sec S (↑(algebraMap R (Localization S)).toMonoidWithZeroHom ↑s)).2 * t)).liftOn
      (fun p => mk p.1 (p.2 * s)) ⋯ =
    mk m t
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_eq_zero {x : ℝ} : log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1

Proof state:
case mp
x : ℝ
h : log x = 0
⊢ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
rcases lt_trichotomy x 0 with (x_lt_zero | rfl | x_gt_zero)

Result:
case mp.inl
x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ x = 0 ∨ x = 1 ∨ x = -1

case mp.inr.inl
h : log 0 = 0
⊢ 0 = 0 ∨ 0 = 1 ∨ 0 = -1

case mp.inr.inr
x : ℝ
h : log x = 0
x_gt_zero : 0 < x
⊢ x = 0 ∨ x = 1 ∨ x = -1

Proof state:
case mp.inl
x : ℝ
h : log (-x) = 0
x_lt_zero : x < 0
⊢ -x = 1

Tactic:
exact eq_one_of_pos_of_log_eq_zero (neg_pos.mpr x_lt_zero) h

Result:
no goals

Proof state:
case mp.inl
x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ -x = 1

Tactic:
rw [← log_neg_eq_log x] at h

Result:
case mp.inl
x : ℝ
h : log (-x) = 0
x_lt_zero : x < 0
⊢ -x = 1

Proof state:
case mp.inl
x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
refine Or.inr (Or.inr (neg_eq_iff_eq_neg.mp ?_))

Result:
case mp.inl
x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ -x = 1

Proof state:
case mpr
x : ℝ
⊢ x = 0 ∨ x = 1 ∨ x = -1 → log x = 0

Tactic:
rintro (rfl | rfl | rfl) <;> simp only [log_one, log_zero, log_neg_eq_log]

Result:
no goals

Proof state:
case mp.inr.inr
x : ℝ
h : log x = 0
x_gt_zero : 0 < x
⊢ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
exact Or.inr (Or.inl (eq_one_of_pos_of_log_eq_zero x_gt_zero h))

Result:
no goals

Proof state:
x : ℝ
⊢ log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
constructor

Result:
case mp
x : ℝ
⊢ log x = 0 → x = 0 ∨ x = 1 ∨ x = -1

case mpr
x : ℝ
⊢ x = 0 ∨ x = 1 ∨ x = -1 → log x = 0

Proof state:
case mp
x : ℝ
⊢ log x = 0 → x = 0 ∨ x = 1 ∨ x = -1

Tactic:
intro h

Result:
case mp
x : ℝ
h : log x = 0
⊢ x = 0 ∨ x = 1 ∨ x = -1

Proof state:
case mp.inr.inl
h : log 0 = 0
⊢ 0 = 0 ∨ 0 = 1 ∨ 0 = -1

Tactic:
exact Or.inl rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem fill_toNat {w : Nat} {v : Bool} :
    (fill w v).toNat = if v = true then 2^w - 1 else 0

Proof state:
w : Nat
v : Bool
⊢ (fill w v).toNat = if v = true then 2 ^ w - 1 else 0

Tactic:
by_cases h : v <;> simp [h]

Result:
no goals
-- Mathlib/Data/DFinsupp/WellFounded.lean
theorem Lex.acc_of_single (hbot : ∀ ⦃i a⦄, ¬s i a 0) [DecidableEq ι]
    [∀ (i) (x : α i), Decidable (x ≠ 0)] (x : Π₀ i, α i) :
    (∀ i ∈ x.support, Acc (DFinsupp.Lex r s) <| single i (x i)) → Acc (DFinsupp.Lex r s) x

Proof state:
case insert
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i), x.support = t → (∀ i ∈ t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : x.support = insert b t
h : ∀ i ∈ insert b t, Acc (DFinsupp.Lex r s) (single i (x i))
⊢ Acc (DFinsupp.Lex r s) (erase b x)

Tactic:
refine ih _ (by rw [support_erase, ht, Finset.erase_insert hb]) fun a ha => ?_

Result:
case insert
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i), x.support = t → (∀ i ∈ t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : x.support = insert b t
h : ∀ i ∈ insert b t, Acc (DFinsupp.Lex r s) (single i (x i))
a : ι
ha : a ∈ t
⊢ Acc (DFinsupp.Lex r s) (single a ((erase b x) a))

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
t : Finset ι
ht : x.support = t
⊢ (∀ i ∈ t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x

Tactic:
revert x

Result:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
t : Finset ι
⊢ ∀ (x : Π₀ (i : ι), α i), x.support = t → (∀ i ∈ t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem sum_mapRange_index.linearMap [DecidableEq ι] {f : ∀ i, β₁ i →ₗ[R] β₂ i}
    {h : ∀ i, β₂ i →ₗ[R] N} {l : Π₀ i, β₁ i} :
    DFinsupp.lsum ℕ h (mapRange.linearMap f l) = DFinsupp.lsum ℕ (fun i => (h i).comp (f i)) l

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
β₁ : ι → Type u_7
β₂ : ι → Type u_8
inst✝⁴ : (i : ι) → AddCommMonoid (β₁ i)
inst✝³ : (i : ι) → AddCommMonoid (β₂ i)
inst✝² : (i : ι) → Module R (β₁ i)
inst✝¹ : (i : ι) → Module R (β₂ i)
inst✝ : DecidableEq ι
f : (i : ι) → β₁ i →ₗ[R] β₂ i
h : (i : ι) → β₂ i →ₗ[R] N
l : Π₀ (i : ι), β₁ i
⊢ ((lsum ℕ) h) ((mapRange.linearMap f) l) = ((lsum ℕ) fun i => h i ∘ₗ f i) l

Tactic:
simpa [DFinsupp.sumAddHom_apply] using sum_mapRange_index fun i => by simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
β₁ : ι → Type u_7
β₂ : ι → Type u_8
inst✝⁴ : (i : ι) → AddCommMonoid (β₁ i)
inst✝³ : (i : ι) → AddCommMonoid (β₂ i)
inst✝² : (i : ι) → Module R (β₁ i)
inst✝¹ : (i : ι) → Module R (β₂ i)
inst✝ : DecidableEq ι
f : (i : ι) → β₁ i →ₗ[R] β₂ i
h : (i : ι) → β₂ i →ₗ[R] N
l : Π₀ (i : ι), β₁ i
i : ι
⊢ (h i) 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
β₁ : ι → Type u_7
β₂ : ι → Type u_8
inst✝⁴ : (i : ι) → AddCommMonoid (β₁ i)
inst✝³ : (i : ι) → AddCommMonoid (β₂ i)
inst✝² : (i : ι) → Module R (β₁ i)
inst✝¹ : (i : ι) → Module R (β₂ i)
inst✝ : DecidableEq ι
f : (i : ι) → β₁ i →ₗ[R] β₂ i
h : (i : ι) → β₂ i →ₗ[R] N
l : Π₀ (i : ι), β₁ i
⊢ ((lsum ℕ) h) ((mapRange.linearMap f) l) = ((lsum ℕ) fun i => h i ∘ₗ f i) l

Tactic:
classical simpa [DFinsupp.sumAddHom_apply] using sum_mapRange_index fun i => by simp

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsBasis.of_isRestriction (hI : N.IsBasis I X) (hNM : N ≤r M) : M.IsBasis I X

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I X R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBasis I X
⊢ M.IsBasis I X

Tactic:
exact ((isBasis_restrict_iff hR).1 hI).1

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
N : Matroid α
hI : N.IsBasis I X
hNM : N ≤r M
⊢ M.IsBasis I X

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Result:
case intro.intro
α : Type u_1
M : Matroid α
I X R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBasis I X
⊢ M.IsBasis I X
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem eq_of_factors_eq_factors {a b : Associates α} (h : a.factors = b.factors) : a = b

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
⊢ a.factors.prod = b.factors.prod

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
⊢ a = b

Tactic:
have : a.factors.prod = b.factors.prod := by rw [h]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
this : a.factors.prod = b.factors.prod
⊢ a = b

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
this : a.factors.prod = b.factors.prod
⊢ a = b

Tactic:
rwa [factors_prod, factors_prod] at this

Result:
no goals