harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/ModelTheory/Order.lean
theorem Term.realize_lt {t₁ t₂ : L.Term (α ⊕ (Fin n))}
    {v : α → M} {xs : Fin n → M} :
    (t₁.lt t₂).Realize v xs ↔ t₁.realize (Sum.elim v xs) < t₂.realize (Sum.elim v xs)

Proof state:
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
t₁ t₂ : L.Term (α ⊕ Fin n)
v : α → M
xs : Fin n → M
⊢ (t₁.lt t₂).Realize v xs ↔ realize (Sum.elim v xs) t₁ < realize (Sum.elim v xs) t₂

Tactic:
simp [Term.lt, lt_iff_le_not_le]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem toSubmodule_eq_top : (N : Submodule R M) = ⊤ ↔ N = ⊤

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ ↑N = ⊤ ↔ N = ⊤

Tactic:
rw [← toSubmodule_inj, top_toSubmodule]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem iterate_id (a : α) : iterate id a = const a :=
  coinduction rfl fun β fr ch => by rw [tail_iterate, tail_const]; exact ch

Proof state:
α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (iterate id a) = fr (const a)
⊢ fr (iterate id a).tail = fr (const a).tail

Tactic:
rw [tail_iterate, tail_const]

Result:
α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (iterate id a) = fr (const a)
⊢ fr (iterate id (id a)) = fr (const a)

Proof state:
α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (iterate id a) = fr (const a)
⊢ fr (iterate id (id a)) = fr (const a)

Tactic:
exact ch

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_ssubset {t : Finset α} : hs.toFinset ⊂ t ↔ s ⊂ t

Proof state:
α : Type u
s : Set α
hs : s.Finite
t : Finset α
⊢ hs.toFinset ⊂ t ↔ s ⊂ ↑t

Tactic:
rw [← Finset.coe_ssubset, Finite.coe_toFinset]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma baseChange_addPolynomial : (W'.baseChange B).toAffine.addPolynomial (f x) (f y) (f ℓ) =
    ((W'.baseChange A).toAffine.addPolynomial x y ℓ).map f

Proof state:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
x y ℓ : A
⊢ (baseChange W' B).toAffine.addPolynomial (f x) (f y) (f ℓ) =
    Polynomial.map (↑f) ((baseChange W' A).toAffine.addPolynomial x y ℓ)

Tactic:
rw [← RingHom.coe_coe, ← map_addPolynomial, map_baseChange]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem join_join {x : Option (Option (Option α))} : x.join.join = (x.map join).join

Proof state:
α : Type u_1
x : Option (Option (Option α))
⊢ x.join.join = (Option.map join x).join

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- `m` is `s`-factored if and only if `m` is nonzero and all prime divisors `≤ m` of `m`
are in `s`. -/
lemma mem_factoredNumbers_iff_forall_le {s : Finset ℕ} {m : ℕ} :
    m ∈ factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ≤ m, p.Prime → p ∣ m → p ∈ s

Proof state:
s : Finset ℕ
m : ℕ
⊢ m ∈ factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s

Tactic:
simp_rw [mem_factoredNumbers, mem_primeFactorsList']

Result:
s : Finset ℕ
m : ℕ
⊢ (m ≠ 0 ∧ ∀ (p : ℕ), Prime p ∧ p ∣ m ∧ m ≠ 0 → p ∈ s) ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s

Proof state:
s : Finset ℕ
m : ℕ
⊢ (m ≠ 0 ∧ ∀ (p : ℕ), Prime p ∧ p ∣ m ∧ m ≠ 0 → p ∈ s) ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s

Tactic:
exact ⟨fun ⟨H₀, H₁⟩ ↦ ⟨H₀, fun p _ hp₂ hp₃ ↦ H₁ p ⟨hp₂, hp₃, H₀⟩⟩,
  fun ⟨H₀, H₁⟩ ↦
    ⟨H₀, fun p ⟨hp₁, hp₂, hp₃⟩ ↦ H₁ p (le_of_dvd (Nat.pos_of_ne_zero hp₃) hp₂) hp₁ hp₂⟩⟩

Result:
no goals
-- Mathlib/Data/Nat/Cast/Defs.lean
theorem cast_one [AddMonoidWithOne R] : ((1 : ℕ) : R) = 1

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑1 = 1

Tactic:
rw [cast_succ, Nat.cast_zero, zero_add]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean
theorem isLeftRegular_of_le_isCancelMulZero (f : LocalizationWithZeroMap S N)
    [IsCancelMulZero M] (h : ∀ ⦃x⦄, x ∈ S → IsRegular x) : IsCancelMulZero N

Proof state:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsRegular x
⊢ IsCancelMulZero N

Tactic:
have : IsLeftCancelMulZero N :=
  leftCancelMulZero_of_le_isLeftRegular f (fun x h' => (h h').left)

Result:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsRegular x
this : IsLeftCancelMulZero N
⊢ IsCancelMulZero N

Proof state:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsRegular x
this : IsLeftCancelMulZero N
⊢ IsCancelMulZero N

Tactic:
exact IsLeftCancelMulZero.to_isCancelMulZero

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
theorem finsuppTensorFinsuppRid_single_tmul_single (a : ι) (b : κ) (m : M) (r : R) :
    finsuppTensorFinsuppRid R M ι κ (Finsupp.single a m ⊗ₜ[R] Finsupp.single b r) =
      Finsupp.single (a, b) (r • m)

Proof state:
R : Type u_1
M : Type u_3
ι : Type u_5
κ : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : ι
b : κ
m : M
r : R
⊢ (finsuppTensorFinsuppRid R M ι κ) (Finsupp.single a m ⊗ₜ[R] Finsupp.single b r) = Finsupp.single (a, b) (r • m)

Tactic:
simp [finsuppTensorFinsuppRid]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `le_inv_mul_iff₀'` for a version with multiplication on the other side. -/
lemma le_inv_mul_iff₀ (hc : 0 < c) : a ≤ c⁻¹ * b ↔ c * a ≤ b where
  mp h

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : PosMulMono G₀
hc : 0 < c
h : a ≤ c⁻¹ * b
⊢ c * a ≤ b

Tactic:
simpa [hc.ne'] using mul_le_mul_of_nonneg_left h hc.le

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : PosMulMono G₀
hc : 0 < c
h : c * a ≤ b
⊢ a ≤ c⁻¹ * b

Tactic:
simpa [hc.ne'] using mul_le_mul_of_nonneg_left h (inv_nonneg.2 hc.le)

Result:
no goals
-- Mathlib/Data/Sum/Interval.lean
theorem Ioo_inr_inl : Ioo (inr b₁) (inl a₂) = ∅

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₂ : α
b₁ : β
⊢ Ioo (inr b₁) (inl a₂) = ∅

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Integral.lean
/-- The non-unital continuous functional calculus commutes with integration. -/
lemma cfcₙ_integral' [TopologicalSpace X] [OpensMeasurableSpace X] (f : X → 𝕜 → 𝕜)
    (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(quasispectrum 𝕜 a, 𝕜)₀]
    (hf : Continuous (fun x => (quasispectrum 𝕜 a).restrict (f x)).uncurry)
    (hf₂ : ∀ x, f x 0 = 0)
    (hbound : ∀ x, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖)
    (hbound_finite_integral : HasFiniteIntegral bound μ) (ha : p a

Proof state:
case refine_2
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : CompleteSpace A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : NonUnitalContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : Continuous (Function.uncurry fun x => (quasispectrum 𝕜 a).restrict (f x))
hf₂ : ∀ (x : X), f x 0 = 0
hbound : ∀ (x : X), ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
⊢ Continuous fun x => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }

Tactic:
let g := ((↑) : C(quasispectrum 𝕜 a, 𝕜)₀ → C(quasispectrum 𝕜 a, 𝕜))

Result:
case refine_2
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : CompleteSpace A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : NonUnitalContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : Continuous (Function.uncurry fun x => (quasispectrum 𝕜 a).restrict (f x))
hf₂ : ∀ (x : X), f x 0 = 0
hbound : ∀ (x : X), ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
g : C(↑(quasispectrum 𝕜 a), 𝕜)₀ → C(↑(quasispectrum 𝕜 a), 𝕜) := toContinuousMap
⊢ Continuous fun x => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ i : Nat, l[i]? = some a

Proof state:
α : Type u_1
a : α
l : List α
h : a ∈ l
n : Nat
w✝ : n < l.length
e : l[n] = a
⊢ ∃ i, l[i]? = some a

Tactic:
exact ⟨n, e ▸ getElem?_eq_getElem _⟩

Result:
no goals

Proof state:
α : Type u_1
a : α
l : List α
h : a ∈ l
⊢ ∃ i, l[i]? = some a

Tactic:
let ⟨n, _, e⟩ := getElem_of_mem h

Result:
α : Type u_1
a : α
l : List α
h : a ∈ l
n : Nat
w✝ : n < l.length
e : l[n] = a
⊢ ∃ i, l[i]? = some a
-- Mathlib/Combinatorics/Quiver/Covering.lean
theorem Prefunctor.symmetrifyStar (u : U) :
    φ.symmetrify.star u =
      (Quiver.symmetrifyStar _).symm ∘ Sum.map (φ.star u) (φ.costar u) ∘
        Quiver.symmetrifyStar u

Proof state:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
⊢ ⇑(Quiver.symmetrifyStar (φ.obj u)) ∘ φ.symmetrify.star u =
    Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)

Tactic:
ext ⟨v, f | g⟩ <;>
  simp only [Quiver.symmetrifyStar, Function.comp_apply] <;>
  erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply] <;>
  simp

Result:
no goals

Proof state:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
⊢ φ.symmetrify.star u =
    ⇑(Quiver.symmetrifyStar (φ.obj u)).symm ∘ Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)

Tactic:
erw [Equiv.eq_symm_comp]

Result:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
⊢ ⇑(Quiver.symmetrifyStar (φ.obj u)) ∘ φ.symmetrify.star u =
    Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)
-- Mathlib/Topology/Order/LeftRight.lean
theorem nhdsLT_sup_nhdsGT (a : α) : 𝓝[<] a ⊔ 𝓝[>] a = 𝓝[≠] a

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[<] a ⊔ 𝓝[>] a = 𝓝[≠] a

Tactic:
rw [← nhdsWithin_union, Iio_union_Ioi]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma coe_div_le : ↑(p / r) ≤ (p / r : ℝ≥0∞)

Proof state:
r p : ℝ≥0
⊢ ↑(p / r) ≤ ↑p / ↑r

Tactic:
simpa only [div_eq_mul_inv, coe_mul] using mul_le_mul_left' coe_inv_le _

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
lemma idemFst_compl : (1 : AddMonoid.End (WithLp p (α × β))) - idemFst = idemSnd

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ 1 - idemFst = idemSnd

Tactic:
rw [← idemFst_add_idemSnd, add_sub_cancel_left]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem and_eq_true_eq_eq_true_and_eq_true (a b : Bool) :
    ((a && b) = true) = (a = true ∧ b = true)

Proof state:
a b : Bool
⊢ ((a && b) = true) = (a = true ∧ b = true)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
theorem Finsupp.linearCombination_one_tmul [DecidableEq ι] {v : ι → M} :
    (linearCombination S ((1 : S) ⊗ₜ[R] v ·)).restrictScalars R =
      (linearCombination R v).lTensor S ∘ₗ (finsuppScalarRight R S ι).symm

Proof state:
case h.h
R : Type u_1
S : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : DecidableEq ι
v : ι → M
a✝ : ι
x✝ : S
⊢ (↑R (linearCombination S fun x => 1 ⊗ₜ[R] v x) ∘ₗ lsingle a✝) x✝ =
    ((lTensor S (linearCombination R v) ∘ₗ ↑(finsuppScalarRight R S ι).symm) ∘ₗ lsingle a✝) x✝

Tactic:
simp [smul_tmul']

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : DecidableEq ι
v : ι → M
⊢ ↑R (linearCombination S fun x => 1 ⊗ₜ[R] v x) = lTensor S (linearCombination R v) ∘ₗ ↑(finsuppScalarRight R S ι).symm

Tactic:
ext

Result:
case h.h
R : Type u_1
S : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : DecidableEq ι
v : ι → M
a✝ : ι
x✝ : S
⊢ (↑R (linearCombination S fun x => 1 ⊗ₜ[R] v x) ∘ₗ lsingle a✝) x✝ =
    ((lTensor S (linearCombination R v) ∘ₗ ↑(finsuppScalarRight R S ι).symm) ∘ₗ lsingle a✝) x✝
-- Mathlib/Data/Real/EReal.lean
theorem natCast_lt_iff {m n : ℕ} : (m : EReal) < (n : EReal) ↔ m < n

Proof state:
m n : ℕ
⊢ ↑m < ↑n ↔ m < n

Tactic:
rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_lt_coe_iff, Nat.cast_lt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_eq_none [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
    (h : containsKey a l = false) : getValueCast? a l = none

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
a : α
h : containsKey a l = false
⊢ getValueCast? a l = none

Tactic:
rwa [← Option.not_isSome_iff_eq_none, ← containsKey_eq_isSome_getValueCast?, Bool.not_eq_true]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_sub_eq_of_lt_left (h : v y < v x) : v (x - y) = v x

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (x - y) = v x

Tactic:
rw [sub_eq_add_neg, map_add_eq_of_lt_left]

Result:
case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (-y) < v x

Proof state:
case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (-y) < v x

Tactic:
rwa [map_neg]

Result:
no goals
-- Mathlib/Topology/AlexandrovDiscrete.lean
lemma closure_iUnion (f : ι → Set α) : closure (⋃ i, f i) = ⋃ i, closure (f i) :=
  compl_injective <| by
    simpa only [← interior_compl, compl_iUnion] using interior_iInter fun i ↦ (f i)ᶜ

Proof state:
ι : Sort u_1
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
f : ι → Set α
⊢ (closure (⋃ i, f i))ᶜ = (⋃ i, closure (f i))ᶜ

Tactic:
simpa only [← interior_compl, compl_iUnion] using interior_iInter fun i ↦ (f i)ᶜ

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_mul_lt_one_iff : a⁻¹ * b < 1 ↔ b < a :=
  _root_.trans inv_mul_lt_iff_lt_mul <| by rw [mul_one]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b : α
⊢ b < a * 1 ↔ b < a

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/Data/DFinsupp/Sigma.lean
theorem sigmaCurry_smul [Monoid γ] [∀ i j, AddMonoid (δ i j)] [∀ i j, DistribMulAction γ (δ i j)]
    (r : γ) (f : Π₀ (i : Σ _, _), δ i.1 i.2) :
    #adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
    we needed to add the `(_ : Π₀ (i) (j), δ i j)` type annotation. -/
    sigmaCurry (r • f) = (r • sigmaCurry f : Π₀ (i) (j), δ i j)

Proof state:
case h.h
ι : Type u
γ : Type w
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → (j : α i) → AddMonoid (δ i j)
inst✝ : (i : ι) → (j : α i) → DistribMulAction γ (δ i j)
r : γ
f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd
i : ι
j : α i
⊢ ((r • f).sigmaCurry i) j = ((r • f.sigmaCurry) i) j

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u
γ : Type w
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → (j : α i) → AddMonoid (δ i j)
inst✝ : (i : ι) → (j : α i) → DistribMulAction γ (δ i j)
r : γ
f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd
⊢ (r • f).sigmaCurry = r • f.sigmaCurry

Tactic:
ext (i j)

Result:
case h.h
ι : Type u
γ : Type w
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → (j : α i) → AddMonoid (δ i j)
inst✝ : (i : ι) → (j : α i) → DistribMulAction γ (δ i j)
r : γ
f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd
i : ι
j : α i
⊢ ((r • f).sigmaCurry i) j = ((r • f.sigmaCurry) i) j
-- Mathlib/Data/Set/Finite/List.lean
lemma finite_length_le : {l : List α | l.length ≤ n}.Finite

Proof state:
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length ≤ n}.Finite

Tactic:
simpa [Nat.lt_succ_iff] using finite_length_lt α (n + 1)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
/-- A variant of `WeierstrassCurve.j_eq_zero_iff_of_char_three` without assuming a reduced ring. -/
lemma j_eq_zero_iff_of_char_three' : W.j = 0 ↔ W.b₂ ^ 6 = 0

Proof state:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 3
⊢ W.j = 0 ↔ W.b₂ ^ 6 = 0

Tactic:
rw [j_of_char_three, Units.mul_right_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem roots_normalize {p : R[X]} : (normalize p).roots = p.roots

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizationMonoid R
p : R[X]
⊢ (normalize p).roots = p.roots

Tactic:
rw [normalize_apply, mul_comm, coe_normUnit, roots_C_mul _ (normUnit (leadingCoeff p)).ne_zero]

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_filter_lt_of_le_right [DecidablePred (· < c)] (hcb : c ≤ b) :
    ((Ico a b).filter fun x => x < c) = Ico a c

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
⊢ filter (fun x => x < c) (Ico a b) = Ico a c

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_right hcb]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
⊢ (Finset.Ico a c).val = Ico a c

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
⊢ (Finset.Ico a c).val = Ico a c

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem BlockTriangular.neg [NegZeroClass R] {M : Matrix m m R}
    (hM : BlockTriangular M b) : BlockTriangular (-M) b :=
  fun _ _ h => by rw [neg_apply, hM h, neg_zero]

Proof state:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝¹ : LT α
inst✝ : NegZeroClass R
M : Matrix m m R
hM : M.BlockTriangular b
x✝¹ x✝ : m
h : b x✝ < b x✝¹
⊢ (-M) x✝¹ x✝ = 0

Tactic:
rw [neg_apply, hM h, neg_zero]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem prod_set' [CommGroup α] (v : Vector α n) (i : Fin n) (a : α) :
    (v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a

Proof state:
α : Type u_1
n : ℕ
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ (v.toList.prod * if hn : ↑i < v.toList.length then v.toList[↑i]⁻¹ * a else 1) = v.toList.prod * (v.get i)⁻¹ * a

Tactic:
simp [get_eq_get_toList, mul_assoc]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a

Tactic:
refine (List.prod_set' v.toList i a).trans ?_

Result:
α : Type u_1
n : ℕ
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ (v.toList.prod * if hn : ↑i < v.toList.length then v.toList[↑i]⁻¹ * a else 1) = v.toList.prod * (v.get i)⁻¹ * a
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
/-- Any entry of any member of `l.ranges` is strictly smaller than `l.sum`. -/
lemma mem_mem_ranges_iff_lt_sum (l : List ℕ) {n : ℕ} :
    (∃ s ∈ l.ranges, n ∈ s) ↔ n < l.sum

Proof state:
l : List ℕ
n : ℕ
⊢ (∃ s ∈ l.ranges, n ∈ s) ↔ n < l.sum

Tactic:
rw [← mem_range, ← ranges_flatten, mem_flatten]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem mem_sup {s t : Submonoid N} {x : N} : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Proof state:
N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
x : N
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
simp only [sup_eq_range, mem_mrange, coprod_apply, coe_subtype, Prod.exists,
  Subtype.exists, exists_prop]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/WithTop.lean
theorem mul_ne_top {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a * b ≠ ⊤

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a * b ≠ ⊤

Tactic:
simp [mul_eq_top_iff, *]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma max_right_comm (a b c : ℕ) : max (max a b) c = max (max a c) b

Proof state:
a b c : ℕ
⊢ max (max a b) c = max (max a c) b

Tactic:
rw [Nat.max_assoc, Nat.max_assoc, b.max_comm]

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem one_def : (1 : R[S⁻¹]) = 1 /ₒ 1

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
⊢ 1 = 1 /ₒ 1

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
⊢ 1 = 1 /ₒ 1

Tactic:
with_unfolding_all rfl

Result:
no goals
-- Mathlib/Order/CompleteLatticeIntervals.lean
theorem coe_biSup : (↑(⨆ i, ⨆ (_ : p i), f i) : α) = ⨆ i, ⨆ (_ : p i), (f i : α)

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
⊢ ↑(⨆ i, ⨆ (_ : p i), f i) = ⨆ i, ⨆ (_ : p i), ↑(f i)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem range_orderEmbOfFin (s : Finset α) {k : ℕ} (h : s.card = k) :
    Set.range (s.orderEmbOfFin h) = s

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ Set.range ⇑(s.orderEmbOfFin h) = ↑s

Tactic:
simp only [orderEmbOfFin, Set.range_comp ((↑) : _ → α) (s.orderIsoOfFin h),
RelEmbedding.coe_trans, Set.image_univ, Finset.orderEmbOfFin, RelIso.range_eq,
  OrderEmbedding.coe_subtype, OrderIso.coe_toOrderEmbedding, eq_self_iff_true,
  Subtype.range_coe_subtype, Finset.setOf_mem, Finset.coe_inj]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem restrict_mass (μ : FiniteMeasure Ω) (A : Set Ω) : (μ.restrict A).mass = μ A

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
A : Set Ω
⊢ (μ.restrict A).mass = μ A

Tactic:
simp only [mass, restrict_apply μ A MeasurableSet.univ, univ_inter]

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem orderEmbOfFin_last {s : Finset α} {k : ℕ} (h : s.card = k) (hz : 0 < k) :
    orderEmbOfFin s h ⟨k - 1, Nat.sub_lt hz (Nat.succ_pos 0)⟩ =
      s.max' (card_pos.mp (h.symm ▸ hz))

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
hz : 0 < k
⊢ (s.orderEmbOfFin h) ⟨k - 1, ⋯⟩ = s.max' ⋯

Tactic:
simp [orderEmbOfFin_apply, max'_eq_sorted_last, h]

Result:
no goals
-- Mathlib/Algebra/Group/Commute/Defs.lean
theorem mul_inv_cancel (h : Commute a b) : a * b * a⁻¹ = b

Proof state:
G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a * b * a⁻¹ = b

Tactic:
rw [h.eq, mul_inv_cancel_right]

Result:
no goals