harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Complex/Basic.lean
theorem ofReal_mul (r s : ℝ) : ((r * s : ℝ) : ℂ) = r * s :=
  Complex.ext_iff.2 <| by simp [ofReal]

Proof state:
r s : ℝ
⊢ (↑(r * s)).re = (↑r * ↑s).re ∧ (↑(r * s)).im = (↑r * ↑s).im

Tactic:
simp [ofReal]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Sized.dual : ∀ {t : Ordnode α}, Sized t → Sized (dual t)
  | nil, _ => ⟨⟩
  | node _ l _ r, ⟨rfl, sl, sr⟩ => ⟨by simp [size_dual, add_comm], Sized.dual sr, Sized.dual sl⟩

Proof state:
α : Type u_1
l : Ordnode α
x✝ : α
r : Ordnode α
sl : l.Sized
sr : r.Sized
⊢ l.size + r.size + 1 = r.dual.size + l.dual.size + 1

Tactic:
simp [size_dual, add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_push_size {a : Array α} {x} : (a.push x)[a.size]? = some x

Proof state:
α : Type u_1
a : Array α
x : α
⊢ (a.push x)[a.size]? = some x

Tactic:
simp [getElem?_push]

Result:
no goals
-- Mathlib/Algebra/Homology/SingleHomology.lean
@[reassoc (attr := simp)]
lemma singleObjCyclesSelfIso_inv_naturality :
    (singleObjCyclesSelfIso c j A).inv ≫ cyclesMap ((single C c j).map f) j =
      f ≫ (singleObjCyclesSelfIso c j B).inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (singleObjCyclesSelfIso c j A).inv ≫ cyclesMap ((single C c j).map f) j = f ≫ (singleObjCyclesSelfIso c j B).inv

Tactic:
rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom, Iso.hom_inv_id_assoc,
  ← singleObjCyclesSelfIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem iff_comp_neg :
    IntervalIntegrable f volume a b ↔ IntervalIntegrable (fun x => f (-x)) volume (-a) (-b)

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
⊢ IntervalIntegrable (fun x => f (-1 * x)) volume (a / -1) (b / -1) ↔
    IntervalIntegrable (fun x => f (-x)) volume (-a) (-b)

Tactic:
simp [div_neg]

Result:
no goals

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
⊢ IntervalIntegrable f volume a b ↔ IntervalIntegrable (fun x => f (-x)) volume (-a) (-b)

Tactic:
rw [← comp_mul_left_iff (neg_ne_zero.2 one_ne_zero)]

Result:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
⊢ IntervalIntegrable (fun x => f (-1 * x)) volume (a / -1) (b / -1) ↔
    IntervalIntegrable (fun x => f (-x)) volume (-a) (-b)
-- Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean
lemma tsum_set_const (c : ℝ≥0∞) : ∑' _ : s, c = s.encard * c

Proof state:
α : Type u_1
s : Set α
c : ℝ≥0∞
⊢ ∑' (x : ↑s), c = ↑s.encard * c

Tactic:
simp [← tsum_set_one, ← ENNReal.tsum_mul_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem drop_append {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l₁ ++ l₂) = drop i l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
i : Nat
⊢ drop (l₁.length + i) (l₁ ++ l₂) = drop i l₂

Tactic:
rw [drop_append_eq_append_drop, drop_eq_nil_of_le] <;>
  simp [Nat.add_sub_cancel_left, Nat.le_add_right]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
@[reassoc]
lemma whiskerRight_app_tensor_app {X Y : J} (f : X ⟶ Y) (X' : J) :
    F.map f ▷ G.obj X' ≫ (α.app Y ⊗ β.app X') =
      (α.app X ⊗ β.app X') ≫ F'.map f ▷ (G'.obj X')

Proof state:
J : Type u_1
inst✝² : Category.{u_3, u_1} J
C : Type u_2
inst✝¹ : Category.{u_4, u_2} C
inst✝ : MonoidalCategory C
F G F' G' : J ⥤ C
α : F ⟶ F'
β : G ⟶ G'
X Y : J
f : X ⟶ Y
X' : J
⊢ F.map f ▷ G.obj X' ≫ (α.app Y ⊗ β.app X') = (α.app X ⊗ β.app X') ≫ F'.map f ▷ G'.obj X'

Tactic:
simpa using tensor_naturality α β f (𝟙 X')

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem one_le_mult {w : InfinitePlace K} : (1 : ℝ) ≤ mult w

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ 1 ≤ w.mult

Tactic:
exact mult_pos

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ 1 ≤ ↑w.mult

Tactic:
rw [← Nat.cast_one, Nat.cast_le]

Result:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ 1 ≤ w.mult
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem hasProd_empty [IsEmpty β] : HasProd f 1

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : IsEmpty β
⊢ HasProd f 1

Tactic:
convert @hasProd_one α β _ _

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem inseparable_iff_forall_isOpen : (x ~ᵢ y) ↔ ∀ s : Set X, IsOpen s → (x ∈ s ↔ y ∈ s)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (x ~ᵢ y) ↔ ∀ (s : Set X), IsOpen s → (x ∈ s ↔ y ∈ s)

Tactic:
simp only [inseparable_iff_specializes_and, specializes_iff_forall_open, ← forall_and, ← iff_def,
  Iff.comm]

Result:
no goals
-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
theorem thickenedIndicatorAux_one (δ : ℝ) (E : Set α) {x : α} (x_in_E : x ∈ E) :
    thickenedIndicatorAux δ E x = 1

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
⊢ thickenedIndicatorAux δ E x = 1

Tactic:
simp [thickenedIndicatorAux, infEdist_zero_of_mem x_in_E, tsub_zero]

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem mem_row_iff {μ : YoungDiagram} {i : ℕ} {c : ℕ × ℕ} : c ∈ μ.row i ↔ c ∈ μ ∧ c.fst = i

Proof state:
μ : YoungDiagram
i : ℕ
c : ℕ × ℕ
⊢ c ∈ μ.row i ↔ c ∈ μ ∧ c.1 = i

Tactic:
simp [row]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma rnDeriv_singularPart (μ ν : Measure α) :
    (μ.singularPart ν).rnDeriv ν =ᵐ[ν] 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ (μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] 0

Tactic:
rw [rnDeriv_eq_zero]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ⟂ₘ ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
exact mutuallySingular_singularPart μ ν

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem linearDepOn_iff' : ¬LinearIndepOn R v s ↔
      ∃ f : ι →₀ R, f ∈ Finsupp.supported R R s ∧ Finsupp.linearCombination R v f = 0 ∧ f ≠ 0

Proof state:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ¬LinearIndepOn R v s ↔ ∃ f ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = 0 ∧ f ≠ 0

Tactic:
simp [linearIndepOn_iff, and_left_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem continuous_sinh : Continuous sinh

Proof state:
⊢ Continuous sinh

Tactic:
change Continuous fun z => (exp z - exp (-z)) / 2

Result:
⊢ Continuous fun z => (cexp z - cexp (-z)) / 2

Proof state:
⊢ Continuous fun z => (cexp z - cexp (-z)) / 2

Tactic:
continuity

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem two_zsmul_oangle_smul_smul_self (x : V) {r₁ r₂ : ℝ} :
    (2 : ℤ) • o.oangle (r₁ • x) (r₂ • x) = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r₁ r₂ : ℝ
⊢ 2 • o.oangle (r₁ • x) (r₂ • x) = 0

Tactic:
by_cases h : r₁ = 0 <;> simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_eq_none_iff_findIdx_eq {xs : List α} {p : α → Bool} :
    xs.findIdx? p = none ↔ xs.findIdx p = xs.length

Proof state:
α : Type u_1
xs : List α
p : α → Bool
⊢ findIdx? p xs = none ↔ findIdx p xs = xs.length

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Moments/ComplexMGF.lean
lemma re_complexMGF_ofReal (x : ℝ) : (complexMGF X μ x).re = mgf X μ x

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
⊢ (complexMGF X μ ↑x).re = mgf X μ x

Tactic:
simp [complexMGF_ofReal]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg (s : ℝ) {b p : ℝ} (hp : 1 < p) (hb : 0 < b) :
    (fun x : ℝ => x ^ s * exp (- b * x ^ p)) =o[atTop] fun x : ℝ => exp (-(1 / 2) * x)

Proof state:
s b p : ℝ
hp : 1 < p
hb : 0 < b
⊢ (fun x => x ^ s * rexp (-b * x ^ p)) =o[atTop] fun x => rexp (-(1 / 2) * x)

Tactic:
apply ((isBigO_refl (fun x : ℝ => x ^ s) atTop).mul_isLittleO
    (exp_neg_mul_rpow_isLittleO_exp_neg hb hp)).trans

Result:
s b p : ℝ
hp : 1 < p
hb : 0 < b
⊢ (fun x => x ^ s * rexp (-x)) =o[atTop] fun x => rexp (-(1 / 2) * x)

Proof state:
s b p : ℝ
hp : 1 < p
hb : 0 < b
⊢ (fun x => x ^ s * rexp (-x)) =o[atTop] fun x => rexp (-(1 / 2) * x)

Tactic:
simpa only [mul_comm] using Real.Gamma_integrand_isLittleO s

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhds_eq_nhdsWithin_sup_nhdsWithin (b : α) {I₁ I₂ : Set α} (hI : Set.univ = I₁ ∪ I₂) :
    nhds b = nhdsWithin b I₁ ⊔ nhdsWithin b I₂

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
hI : univ = I₁ ∪ I₂
⊢ 𝓝 b = 𝓝[I₁] b ⊔ 𝓝[I₂] b

Tactic:
rw [← nhdsWithin_univ b, hI, nhdsWithin_union]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
theorem HasDerivWithinAt.log (hf : HasDerivWithinAt f f' s x) (hx : f x ≠ 0) :
    HasDerivWithinAt (fun y => log (f y)) (f' / f x) s x

Proof state:
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.log (f y)) ((f x)⁻¹ * f') s x

Tactic:
exact (hasDerivAt_log hx).comp_hasDerivWithinAt x hf

Result:
no goals

Proof state:
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.log (f y)) (f' / f x) s x

Tactic:
rw [div_eq_inv_mul]

Result:
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.log (f y)) ((f x)⁻¹ * f') s x
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_cos_add_sin_mul_I_eq_toIocMod (θ : ℝ) :
    arg (cos θ + sin θ * I) = toIocMod Real.two_pi_pos (-π) θ

Proof state:
θ : ℝ
⊢ (cos ↑θ + sin ↑θ * I).arg = toIocMod Real.two_pi_pos (-π) θ

Tactic:
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_eq_toIocMod zero_lt_one]

Result:
no goals
-- Mathlib/Algebra/Ring/Basic.lean
theorem inv_neg' (a : α) : (-a)⁻¹ = -a⁻¹

Proof state:
α : Type u_2
inst✝¹ : Group α
inst✝ : HasDistribNeg α
a : α
⊢ (-a)⁻¹ = -a⁻¹

Tactic:
rw [eq_comm, eq_inv_iff_mul_eq_one, neg_mul, mul_neg, neg_neg, inv_mul_cancel]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem map_le_map_iff' {f : G →* N} {H K : Subgroup G} :
    H.map f ≤ K.map f ↔ H ⊔ f.ker ≤ K ⊔ f.ker

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
⊢ map f H ≤ map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker

Tactic:
simp only [map_le_map_iff, sup_le_iff, le_sup_right, and_true]

Result:
no goals
-- Mathlib/FieldTheory/Finiteness.lean
theorem range_finsetBasis [IsNoetherian K V] :
    Set.range (finsetBasis K V) = Basis.ofVectorSpaceIndex K V

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsNoetherian K V
⊢ Set.range ⇑(finsetBasis K V) = Basis.ofVectorSpaceIndex K V

Tactic:
rw [finsetBasis, Basis.range_reindex, Basis.range_ofVectorSpace]

Result:
no goals
-- Mathlib/Order/Filter/Tendsto.lean
theorem Filter.map_mapsTo_Iic_iff_mapsTo {s : Set α} {t : Set β} {m : α → β} :
    MapsTo (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 t) ↔ MapsTo m s t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ MapsTo m s t

Tactic:
rw [map_mapsTo_Iic_iff_tendsto, tendsto_principal_principal, MapsTo]

Result:
no goals
-- Mathlib/Data/Int/Log.lean
theorem log_of_right_le_zero (b : ℕ) {r : R} (hr : r ≤ 0) : log b r = 0

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ log b r = 0

Tactic:
rw [log_of_right_le_one _ (hr.trans zero_le_one),
  Nat.clog_of_right_le_one ((Nat.ceil_eq_zero.mpr <| inv_nonpos.2 hr).trans_le zero_le_one),
  Int.ofNat_zero, neg_zero]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem ne_int (h : Irrational x) (m : ℤ) : x ≠ m

Proof state:
x : ℝ
h : Irrational x
m : ℤ
⊢ x ≠ ↑↑m

Tactic:
exact h.ne_rat _

Result:
no goals

Proof state:
x : ℝ
h : Irrational x
m : ℤ
⊢ x ≠ ↑m

Tactic:
rw [← Rat.cast_intCast]

Result:
x : ℝ
h : Irrational x
m : ℤ
⊢ x ≠ ↑↑m
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem aemeasurable_comp_iff {f : α → β} (hf : MeasurePreserving f μa μb)
    (h₂ : MeasurableEmbedding f) {g : β → γ} : AEMeasurable (g ∘ f) μa ↔ AEMeasurable g μb

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
g : β → γ
⊢ AEMeasurable (g ∘ f) μa ↔ AEMeasurable g μb

Tactic:
rw [← hf.map_eq, h₂.aemeasurable_map_iff]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem isClosed_image (h : X ≃ₜ Y) {s : Set X} : IsClosed (h '' s) ↔ IsClosed s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ IsClosed (⇑h '' s) ↔ IsClosed s

Tactic:
rw [← preimage_symm, isClosed_preimage]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Map.lean
theorem map_le_size {aig : AIG α} (target : MapTarget aig len) :
    aig.decls.size ≤ (map aig target).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : MapTarget aig len
⊢ aig.decls.size ≤ (map aig target).aig.decls.size

Tactic:
unfold map

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : MapTarget aig len
⊢ aig.decls.size ≤ (map.go aig 0 ⋯ empty target.vec target.func).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : MapTarget aig len
⊢ aig.decls.size ≤ (map.go aig 0 ⋯ empty target.vec target.func).aig.decls.size

Tactic:
apply map.go_le_size

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem succ_max_succ (x y) : max (succ x) (succ y) = succ (max x y)

Proof state:
case inl
x y : Nat
h : x ≤ y
⊢ max x.succ y.succ = (max x y).succ

Tactic:
rw [Nat.max_eq_right h, Nat.max_eq_right (Nat.succ_le_succ h)]

Result:
no goals

Proof state:
x y : Nat
⊢ max x.succ y.succ = (max x y).succ

Tactic:
cases Nat.le_total x y with
| inl h => rw [Nat.max_eq_right h, Nat.max_eq_right (Nat.succ_le_succ h)]
| inr h => rw [Nat.max_eq_left h, Nat.max_eq_left (Nat.succ_le_succ h)]

Result:
no goals

Proof state:
case inr
x y : Nat
h : y ≤ x
⊢ max x.succ y.succ = (max x y).succ

Tactic:
rw [Nat.max_eq_left h, Nat.max_eq_left (Nat.succ_le_succ h)]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_compl_add_restrict (hs : MeasurableSet s) : μ.restrict sᶜ + μ.restrict s = μ

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ μ.restrict sᶜ + μ.restrict s = μ

Tactic:
rw [add_comm, restrict_add_restrict_compl hs]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Root.lean
@[simp] lemma floorRoot_zero_left (a : ℕ) : floorRoot 0 a = 0

Proof state:
a : ℕ
⊢ floorRoot 0 a = 0

Tactic:
simp [floorRoot]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem exists_mul_sub_mem_of_sub_one_mem_jacobson {I : Ideal R} (r : R) (h : r - 1 ∈ jacobson I) :
    ∃ s, s * r - 1 ∈ I

Proof state:
case h.e'_2.h.h.e'_5.h.e'_5.h.e'_6
R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r - 1 ∈ I.jacobson
x✝ : R
⊢ r = r - 1 + 1

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r - 1 ∈ I.jacobson
⊢ ∃ s, s * r - 1 ∈ I

Tactic:
convert exists_mul_add_sub_mem_of_mem_jacobson _ h

Result:
case h.e'_2.h.h.e'_5.h.e'_5.h.e'_6
R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r - 1 ∈ I.jacobson
x✝ : R
⊢ r = r - 1 + 1
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma Y_sub_negPolynomial : Y - W'.negPolynomial = W'.polynomialY

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - W'.negPolynomial = W'.polynomialY

Tactic:
rw [← Y_sub_polynomialY, sub_sub_cancel]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_fuzzy_neg_iff {x y : PGame} : -x ‖ -y ↔ x ‖ y

Proof state:
x y : PGame
⊢ -x ‖ -y ↔ x ‖ y

Tactic:
rw [Fuzzy, Fuzzy, neg_lf_neg_iff, neg_lf_neg_iff, and_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Basic.lean
theorem le_map_add_map_div [Group α] [AddCommSemigroup β] [LE β] [MulLEAddHomClass F α β] (f : F)
    (a b : α) : f a ≤ f b + f (a / b)

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommSemigroup β
inst✝¹ : LE β
inst✝ : MulLEAddHomClass F α β
f : F
a b : α
⊢ f a ≤ f b + f (a / b)

Tactic:
simpa only [add_comm, div_mul_cancel] using map_mul_le_add f (a / b) b

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem mul_comm : ∀ (a b : ZNum), a * b = b * a

Proof state:
⊢ ∀ (a b : ZNum), a * b = b * a

Tactic:
transfer

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_cons_of_false [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β}
    (h : (k == a) = false) : getValue? a (⟨k, v⟩ :: l) = getValue? a l

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = false
⊢ getValue? a (⟨k, v⟩ :: l) = getValue? a l

Tactic:
simp [getValue?, h]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
theorem eval_C {c : K} : eval f a (C c) = f c

Proof state:
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
c : K
⊢ eval f a (C c) = f c

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem Subsingleton.einfsep (hs : s.Subsingleton) : s.einfsep = ∞

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Subsingleton
⊢ s.einfsep = ⊤

Tactic:
rw [einfsep_top]

Result:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Subsingleton
⊢ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ⊤

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Subsingleton
⊢ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ⊤

Tactic:
exact fun _ hx _ hy hxy => (hxy <| hs hx hy).elim

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem get_set_same (v : Vector α n) (i : Fin n) (a : α) : (v.set i a).get i = a

Proof state:
case mk.mk
α : Type u_1
n : ℕ
a : α
val✝¹ : List α
property✝ : val✝¹.length = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ (set ⟨val✝¹, property✝⟩ ⟨val✝, isLt✝⟩ a).get ⟨val✝, isLt✝⟩ = a

Tactic:
simp [Vector.set, get_eq_get_toList]

Result:
no goals

Proof state:
case mk
α : Type u_1
n : ℕ
i : Fin n
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ (set ⟨val✝, property✝⟩ i a).get i = a

Tactic:
cases i

Result:
case mk.mk
α : Type u_1
n : ℕ
a : α
val✝¹ : List α
property✝ : val✝¹.length = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ (set ⟨val✝¹, property✝⟩ ⟨val✝, isLt✝⟩ a).get ⟨val✝, isLt✝⟩ = a

Proof state:
α : Type u_1
n : ℕ
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).get i = a

Tactic:
cases v

Result:
case mk
α : Type u_1
n : ℕ
i : Fin n
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ (set ⟨val✝, property✝⟩ i a).get i = a
-- Mathlib/Algebra/Module/SpanRank.lean
/-- The elements of the generators are in the submodule. -/
lemma FG.generators_mem (p : Submodule R M) : generators p ⊆ p

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p.generators ⊆ ↑p

Tactic:
nth_rw 2 [← span_generators p]

Result:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p.generators ⊆ ↑(span R p.generators)

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p.generators ⊆ ↑(span R p.generators)

Tactic:
exact subset_span (s := generators p)

Result:
no goals
-- Mathlib/CategoryTheory/Functor/FullyFaithful.lean
theorem preimageIso_mapIso (f : X ≅ Y) : F.preimageIso (F.mapIso f) = f

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
inst✝¹ : F.Full
inst✝ : F.Faithful
f : X ≅ Y
⊢ F.preimageIso (F.mapIso f) = f

Tactic:
ext

Result:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
inst✝¹ : F.Full
inst✝ : F.Faithful
f : X ≅ Y
⊢ (F.preimageIso (F.mapIso f)).hom = f.hom

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
inst✝¹ : F.Full
inst✝ : F.Faithful
f : X ≅ Y
⊢ (F.preimageIso (F.mapIso f)).hom = f.hom

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompMap.lean
lemma snd_comp (κ : Kernel α β) (η : Kernel β (γ × δ)) : (η ∘ₖ κ).snd = η.snd ∘ₖ κ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β (γ × δ)
⊢ (η ∘ₖ κ).snd = η.snd ∘ₖ κ

Tactic:
simp_rw [snd_eq, map_comp κ η _]

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem seminormAux_zero (k n : ℕ) : (0 : 𝓢(E, F)).seminormAux k n = 0 :=
  le_antisymm (seminormAux_le_bound k n _ rfl.le fun _ => by simp [Pi.zero_def])
    (seminormAux_nonneg _ _ _)

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
x✝ : E
⊢ ‖x✝‖ ^ k * ‖iteratedFDeriv ℝ n (⇑0) x✝‖ ≤ 0

Tactic:
simp [Pi.zero_def]

Result:
no goals
-- Mathlib/Control/Bifunctor.lean
theorem comp_fst {α₀ α₁ α₂ β} (f : α₀ → α₁) (f' : α₁ → α₂) (x : F α₀ β) :
    fst f' (fst f x) = fst (f' ∘ f) x

Proof state:
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α₀ α₁ α₂ : Type u₀
β : Type u₁
f : α₀ → α₁
f' : α₁ → α₂
x : F α₀ β
⊢ fst f' (fst f x) = fst (f' ∘ f) x

Tactic:
simp [fst, bimap_bimap]

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rdropWhile_eq_nil_iff : rdropWhile p l = [] ↔ ∀ x ∈ l, p x

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
simp [rdropWhile]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem Iic_iInf (f : ι → α) : Iic (⨅ i, f i) = ⋂ i, Iic (f i) :=
  ext fun _ => by simp only [mem_Iic, le_iInf_iff, mem_iInter]

Proof state:
α : Type u_1
ι : Sort u_5
inst✝ : CompleteLattice α
f : ι → α
x✝ : α
⊢ x✝ ∈ Iic (⨅ i, f i) ↔ x✝ ∈ ⋂ i, Iic (f i)

Tactic:
simp only [mem_Iic, le_iInf_iff, mem_iInter]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem repr_reindex_apply (i' : ι') : (b.reindex e).repr x i' = b.repr x (e.symm i') :=
  show (Finsupp.domLCongr e : _ ≃ₗ[R] _) (b.repr x) i' = _ by simp

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
e : ι ≃ ι'
i' : ι'
⊢ ((Finsupp.domLCongr e) (b.repr x)) i' = (b.repr x) (e.symm i')

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
theorem unitors_inv_equal : (λ_ (𝟙_ C)).inv = (ρ_ (𝟙_ C)).inv

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).inv = (ρ_ (𝟙_ C)).inv

Tactic:
monoidal_coherence

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem toEnd' (it : Iterator) : ValidFor it.s.1.reverse [] it.toEnd

Proof state:
it : Iterator
⊢ { s := it.s, i := it.s.endPos }.s.data = it.s.data.reverse.reverseAux []

Tactic:
simp [List.reverseAux_eq]

Result:
no goals

Proof state:
it : Iterator
⊢ { s := it.s, i := it.s.endPos }.i.byteIdx = utf8Len it.s.data.reverse

Tactic:
simp [endPos, utf8ByteSize]

Result:
no goals

Proof state:
it : Iterator
⊢ ValidFor it.s.data.reverse [] { s := it.s, i := it.s.endPos }

Tactic:
exact .of_eq _ (by simp [List.reverseAux_eq]) (by simp [endPos, utf8ByteSize])

Result:
no goals

Proof state:
it : Iterator
⊢ ValidFor it.s.data.reverse [] it.toEnd

Tactic:
simp only [Iterator.toEnd]

Result:
it : Iterator
⊢ ValidFor it.s.data.reverse [] { s := it.s, i := it.s.endPos }