harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem trans {R : Type*} (A M : Type*) [Semiring R] [Semiring A] [Module R A]
    [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] :
    ∀ [Module.Finite R A] [Module.Finite A M], Module.Finite R M
  | ⟨⟨s, hs⟩⟩, ⟨⟨t, ht⟩⟩ =>
    ⟨Submodule.fg_def.2
        ⟨Set.image2 (· • ·) (↑s : Set A) (↑t : Set M),
          Set.Finite.image2 _ s.finite_toSet t.finite_toSet, by
          erw [Set.image2_smul, Submodule.span_smul_of_span_eq_top hs (↑t : Set M), ht,
            Submodule.restrictScalars_top]⟩⟩

Proof state:
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : Finset A
hs : span R ↑s = ⊤
t : Finset M
ht : span A ↑t = ⊤
⊢ span R (image2 (fun x1 x2 => x1 • x2) ↑s ↑t) = ⊤

Tactic:
erw [Set.image2_smul, Submodule.span_smul_of_span_eq_top hs (↑t : Set M), ht,
  Submodule.restrictScalars_top]

Result:
no goals
-- Mathlib/Topology/Order.lean
lemma tendsto_nhds_generateFrom_iff {β : Type*} {m : α → β} {f : Filter α} {g : Set (Set β)}
    {b : β} : Tendsto m f (@nhds β (generateFrom g) b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f

Proof state:
α : Type u
β : Type u_1
m : α → β
f : Filter α
g : Set (Set β)
b : β
⊢ (∀ i ∈ g, b ∈ i → ∀ᶠ (a : α) in f, m a ∈ i) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type u_1
m : α → β
f : Filter α
g : Set (Set β)
b : β
⊢ Tendsto m f (𝓝 b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f

Tactic:
simp only [nhds_generateFrom, @forall_swap (b ∈ _), tendsto_iInf, mem_setOf_eq, and_imp,
  tendsto_principal]

Result:
α : Type u
β : Type u_1
m : α → β
f : Filter α
g : Set (Set β)
b : β
⊢ (∀ i ∈ g, b ∈ i → ∀ᶠ (a : α) in f, m a ∈ i) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f
-- Mathlib/Analysis/Convex/Body.lean
theorem hausdorffEdist_ne_top {K L : ConvexBody V} : EMetric.hausdorffEdist (K : Set V) L ≠ ⊤

Proof state:
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NormedSpace ℝ V
K L : ConvexBody V
⊢ EMetric.hausdorffEdist ↑K ↑L ≠ ⊤

Tactic:
apply_rules [Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded, ConvexBody.nonempty,
  ConvexBody.isBounded]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
lemma toList_eq_nil : p.toList = [] ↔ p = 0

Proof state:
p : DyckWord
⊢ ↑p = [] ↔ p = 0

Tactic:
rw [DyckWord.ext_iff]

Result:
p : DyckWord
⊢ ↑p = [] ↔ ↑p = ↑0

Proof state:
p : DyckWord
⊢ ↑p = [] ↔ ↑p = ↑0

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_cons_of_neg {p : α → Bool} {a : α} {l} (pa : ¬ p a) :
    filter p (a :: l) = filter p l

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ filter p (a :: l) = filter p l

Tactic:
rw [filter, eq_false_of_ne_true pa]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem nim_fuzzy_zero_of_ne_zero {o : Ordinal} (ho : o ≠ 0) : nim o ‖ 0

Proof state:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ ∃ j, (nim o).moveRight j ≤ 0

Tactic:
use toRightMovesNim ⟨0, Ordinal.pos_iff_ne_zero.2 ho⟩

Result:
case h
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ (nim o).moveRight (toRightMovesNim ⟨0, ⋯⟩) ≤ 0

Proof state:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ nim o ‖ 0

Tactic:
rw [Impartial.fuzzy_zero_iff_lf, lf_zero_le]

Result:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ ∃ j, (nim o).moveRight j ≤ 0

Proof state:
case h
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ (nim o).moveRight (toRightMovesNim ⟨0, ⋯⟩) ≤ 0

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem separable_of_subsingleton [Subsingleton R] (f : R[X]) : f.Separable

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : Subsingleton R
f : R[X]
⊢ f.Separable

Tactic:
simp [Separable, IsCoprime, eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_symmDiff_cancel_right : b ∆ a ∆ a = b

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b ∆ a ∆ a = b

Tactic:
simp [symmDiff_assoc]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem cycleRange_zero (n : ℕ) [NeZero n] : cycleRange (0 : Fin n) = 1

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ cycleRange 0 = 1

Tactic:
ext j

Result:
case H.h
n : ℕ
inst✝ : NeZero n
j : Fin n
⊢ ↑((cycleRange 0) j) = ↑(1 j)

Proof state:
case H.h.inr
n : ℕ
inst✝ : NeZero n
j : Fin n
hj : 0 < j
⊢ ↑((cycleRange 0) j) = ↑(1 j)

Tactic:
rw [cycleRange_of_gt hj, one_apply]

Result:
no goals

Proof state:
case H.h.inl
n : ℕ
inst✝ : NeZero n
⊢ ↑((cycleRange 0) 0) = ↑(1 0)

Tactic:
simp

Result:
no goals

Proof state:
case H.h
n : ℕ
inst✝ : NeZero n
j : Fin n
⊢ ↑((cycleRange 0) j) = ↑(1 j)

Tactic:
rcases (Fin.zero_le' j).eq_or_lt with rfl | hj

Result:
case H.h.inl
n : ℕ
inst✝ : NeZero n
⊢ ↑((cycleRange 0) 0) = ↑(1 0)

case H.h.inr
n : ℕ
inst✝ : NeZero n
j : Fin n
hj : 0 < j
⊢ ↑((cycleRange 0) j) = ↑(1 j)
-- Mathlib/Data/Multiset/Nodup.lean
theorem Nodup.add_iff (d₁ : Nodup s) (d₂ : Nodup t) : Nodup (s + t) ↔ Disjoint s t

Proof state:
α : Type u_1
s t : Multiset α
d₁ : s.Nodup
d₂ : t.Nodup
⊢ (s + t).Nodup ↔ _root_.Disjoint s t

Tactic:
simp [nodup_add, d₁, d₂]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_comp_neg (hf : ContinuousOn f ((- ·) '' (σₙ R a))

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹³ : CommRing R
inst✝¹² : Nontrivial R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
inst✝ : UniqueHom R A
hf : autoParam (ContinuousOn f ((fun x => -x) '' σₙ R a)) _auto✝
h0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfcₙ (fun x => f (-x)) a = cfcₙ f (-a)

Tactic:
rw [cfcₙ_comp' .., cfcₙ_neg_id _]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem setLIntegral_withDensity_eq_setLIntegral_mul (μ : Measure α) {f g : α → ℝ≥0∞}
    (hf : Measurable f) (hg : Measurable g) {s : Set α} (hs : MeasurableSet s) :
    ∫⁻ x in s, g x ∂μ.withDensity f = ∫⁻ x in s, (f * g) x ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, g x ∂μ.withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ

Tactic:
rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul _ hf hg]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem lift'_neBot_iff (hh : Monotone h) : NeBot (f.lift' h) ↔ ∀ s ∈ f, (h s).Nonempty :=
  calc
    NeBot (f.lift' h) ↔ ∀ s ∈ f, NeBot (𝓟 (h s)) := lift_neBot_iff (monotone_principal.comp hh)
    _ ↔ ∀ s ∈ f, (h s).Nonempty

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
hh : Monotone h
⊢ (∀ s ∈ f, (𝓟 (h s)).NeBot) ↔ ∀ s ∈ f, (h s).Nonempty

Tactic:
simp only [principal_neBot_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue!_of_perm [BEq α] [PartialEquivBEq α] [Inhabited β] {l l' : List ((_ : α) × β)}
    {a : α} (hl : DistinctKeys l) (h : Perm l l') : getValue! a l = getValue! a l'

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : PartialEquivBEq α
inst✝ : Inhabited β
l l' : List ((_ : α) × β)
a : α
hl : DistinctKeys l
h : l.Perm l'
⊢ getValue! a l = getValue! a l'

Tactic:
simp only [getValue!_eq_getValue?, getValue?_of_perm hl h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.sup {β} [NormedLatticeAddCommGroup β] {f g : α → β} (hf : Integrable f μ)
    (hg : Integrable g μ) : Integrable (f ⊔ g) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : NormedLatticeAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f ⊔ g) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf hg ⊢

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : NormedLatticeAddCommGroup β
f g : α → β
hf : MemLp f 1 μ
hg : MemLp g 1 μ
⊢ MemLp (f ⊔ g) 1 μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : NormedLatticeAddCommGroup β
f g : α → β
hf : MemLp f 1 μ
hg : MemLp g 1 μ
⊢ MemLp (f ⊔ g) 1 μ

Tactic:
exact hf.sup hg

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem partialProd_zero (f : Fin n → α) : partialProd f 0 = 1

Proof state:
α : Type u_1
inst✝ : Monoid α
n : ℕ
f : Fin n → α
⊢ partialProd f 0 = 1

Tactic:
simp [partialProd]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem degree_C_mul_T (n : ℤ) (a : R) (a0 : a ≠ 0) : degree (C a * T n) = n

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ {n}.max = ↑n

Tactic:
exact Finset.max_singleton

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ (C a * T n).degree = ↑n

Tactic:
rw [degree, support_C_mul_T_of_ne_zero a0 n]

Result:
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ {n}.max = ↑n
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma comp_apply {R S T : CommSemiRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : R) :
    (f ≫ g) r = g (f r)

Proof state:
R S T : CommSemiRingCat
f : R ⟶ S
g : S ⟶ T
r : ↑R
⊢ (ConcreteCategory.hom (f ≫ g)) r = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) r)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_const_add [AddCommSemigroup G] [Add H] [AddConstMapClass F G H a b]
    (f : F) (x : G) : f (a + x) = f x + b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddCommSemigroup G
inst✝¹ : Add H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
⊢ f (a + x) = f x + b

Tactic:
rw [add_comm, map_add_const]

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem lift_comp_map (h : MultilinearMap R t E) :
    lift h ∘ₗ map f = lift (h.compLinearMap f)

Proof state:
case H.H
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
h : MultilinearMap R t E
x✝ : (i : ι) → s i
⊢ ((lift h ∘ₗ map f).compMultilinearMap (tprod R)) x✝ = ((lift (h.compLinearMap f)).compMultilinearMap (tprod R)) x✝

Tactic:
simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, Function.comp_apply,
  map_tprod, lift.tprod, MultilinearMap.compLinearMap_apply]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
h : MultilinearMap R t E
⊢ lift h ∘ₗ map f = lift (h.compLinearMap f)

Tactic:
ext

Result:
case H.H
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
h : MultilinearMap R t E
x✝ : (i : ι) → s i
⊢ ((lift h ∘ₗ map f).compMultilinearMap (tprod R)) x✝ = ((lift (h.compLinearMap f)).compMultilinearMap (tprod R)) x✝
-- Mathlib/Computability/Tape.lean
theorem Tape.move_right_nth {Γ} [Inhabited Γ] (T : Tape Γ) (i : ℤ) :
    (T.move Dir.right).nth i = T.nth (i + 1)

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℤ
⊢ (move Dir.right T).nth i = (move Dir.left (move Dir.right T)).nth (i + 1)

Tactic:
rw [Tape.move_left_nth, add_sub_cancel_right]

Result:
no goals

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℤ
⊢ (move Dir.right T).nth i = T.nth (i + 1)

Tactic:
conv => rhs; rw [← T.move_right_left]

Result:
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℤ
⊢ (move Dir.right T).nth i = (move Dir.left (move Dir.right T)).nth (i + 1)
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem absolutelyContinuous_map_div_left (g : G) : μ ≪ map (fun h => g / h) μ

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ μ ≪ map (fun h => g / h) μ

Tactic:
simp_rw [div_eq_mul_inv]

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ μ ≪ map (fun h => g * h⁻¹) μ

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ μ ≪ map (fun x => g * x) (map Inv.inv μ)

Tactic:
conv_lhs => rw [← map_mul_left_eq_self μ g]

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ map (fun x => g * x) μ ≪ map (fun x => g * x) (map Inv.inv μ)

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ map (fun x => g * x) μ ≪ map (fun x => g * x) (map Inv.inv μ)

Tactic:
exact (absolutelyContinuous_inv μ).map (measurable_const_mul g)

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ μ ≪ map (fun h => g * h⁻¹) μ

Tactic:
erw [← map_map (measurable_const_mul g) measurable_inv]

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ μ ≪ map (fun x => g * x) (map Inv.inv μ)
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem val_pow : ∀ (y : HomogeneousLocalization 𝒜 x) (n : ℕ), (y ^ n).val = y.val ^ n :=
  Quotient.ind' fun y n ↦ by rw [← mk_pow, val_mk, val_mk, Localization.mk_pow]; rfl

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ Localization.mk ↑(y ^ n).num ⟨↑(y ^ n).den, ⋯⟩ = Localization.mk (↑y.num ^ n) (⟨↑y.den, ⋯⟩ ^ n)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ (Quotient.mk'' y ^ n).val = val (Quotient.mk'' y) ^ n

Tactic:
rw [← mk_pow, val_mk, val_mk, Localization.mk_pow]

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ Localization.mk ↑(y ^ n).num ⟨↑(y ^ n).den, ⋯⟩ = Localization.mk (↑y.num ^ n) (⟨↑y.den, ⋯⟩ ^ n)
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_reindex (e₁ : l ≃ m) (e₂ : n ≃ o) (A : Matrix l n R) :
    rank (reindex e₁ e₂ A) = rank A

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : CommRing R
e₁ : l ≃ m
e₂ : n ≃ o
A : Matrix l n R
⊢ ((reindex e₁ e₂) A).rank = A.rank

Tactic:
rw [rank, rank, mulVecLin_reindex, LinearMap.range_comp, LinearMap.range_comp,
  LinearEquiv.range, Submodule.map_top, LinearEquiv.finrank_map_eq]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem ret_bind (a : α) (f : α → Seq1 β) : bind (ret a) f = f a

Proof state:
case mk
α : Type u
β : Type v
a✝ : α
f : α → Seq1 β
a : β
s : Seq β
⊢ join ((a, s), nil) = (a, s)

Tactic:
cases s <;> simp

Result:
no goals

Proof state:
α : Type u
β : Type v
a : α
f : α → Seq1 β
⊢ join (f a, nil) = f a

Tactic:
obtain ⟨a, s⟩ := f a

Result:
case mk
α : Type u
β : Type v
a✝ : α
f : α → Seq1 β
a : β
s : Seq β
⊢ join ((a, s), nil) = (a, s)

Proof state:
α : Type u
β : Type v
a : α
f : α → Seq1 β
⊢ (ret a).bind f = f a

Tactic:
simp only [bind, map, ret.eq_1, map_nil]

Result:
α : Type u
β : Type v
a : α
f : α → Seq1 β
⊢ join (f a, nil) = f a
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_erase [LawfulBEq α] (h : m.1.WF) {k a : α} {fallback : β a} :
    (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k a : α
fallback : β a
⊢ (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback

Tactic:
simp_to_model [erase] using List.getValueCastD_eraseKey

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem cospanExt_app_one : (cospanExt iX iY iZ wf wg).app WalkingCospan.one = iZ

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).app WalkingCospan.one = iZ

Tactic:
dsimp [cospanExt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem isHashSelf_foldl_reinsertAux [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
    (l : List ((a : α) × β a)) (target : { d : Array (AssocList α β) // 0 < d.size }) :
    IsHashSelf target.1 →
      IsHashSelf (l.foldl (fun acc p => reinsertAux hash acc p.1 p.2) target).1

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
target : { d // 0 < d.size }
⊢ IsHashSelf target.val → IsHashSelf (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target l).val

Tactic:
induction l generalizing target

Result:
case nil
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
target : { d // 0 < d.size }
⊢ IsHashSelf target.val → IsHashSelf (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target []).val

case cons
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ :
  ∀ (target : { d // 0 < d.size }),
    IsHashSelf target.val → IsHashSelf (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target tail✝).val
target : { d // 0 < d.size }
⊢ IsHashSelf target.val → IsHashSelf (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target (head✝ :: tail✝)).val

Proof state:
case cons
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ :
  ∀ (target : { d // 0 < d.size }),
    IsHashSelf target.val → IsHashSelf (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target tail✝).val
target : { d // 0 < d.size }
⊢ IsHashSelf target.val → IsHashSelf (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target (head✝ :: tail✝)).val

Tactic:
next k v _ ih => exact fun h => ih _ (isHashSelf_reinsertAux _ _ _ h)

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
target : { d // 0 < d.size }
⊢ IsHashSelf target.val → IsHashSelf (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target []).val

Tactic:
simp [Id.run]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
k : LawfulHashable α
v : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih :
  ∀ (target : { d // 0 < d.size }),
    IsHashSelf target.val → IsHashSelf (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target tail✝).val
target : { d // 0 < d.size }
⊢ IsHashSelf target.val → IsHashSelf (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target (v :: tail✝)).val

Tactic:
exact fun h => ih _ (isHashSelf_reinsertAux _ _ _ h)

Result:
no goals
-- Mathlib/Topology/UnitInterval.lean
lemma abs_sub_addNSMul_le (hδ : 0 ≤ δ) {t : Icc a b} (n : ℕ)
    (ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n+1))) :
    (|t - addNSMul h δ n| : α) ≤ δ :=
  calc
    (|t - addNSMul h δ n| : α) = t - addNSMul h δ n            := abs_eq_self.2 <| sub_nonneg.2 ht.1
    _ ≤ projIcc a b h (a + (n+1) • δ) - addNSMul h δ n

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
t : ↑(Icc a b)
n : ℕ
ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))
⊢ |a + (n + 1) • δ - (a + n • δ)| ≤ δ

Tactic:
rw [add_sub_add_comm, sub_self, zero_add, succ_nsmul', add_sub_cancel_right]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
t : ↑(Icc a b)
n : ℕ
ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))
⊢ |δ| ≤ δ

Proof state:
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
t : ↑(Icc a b)
n : ℕ
ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))
⊢ ↑t ≤ ↑(projIcc a b h (a + (n + 1) • δ))

Tactic:
exact ht.2

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
t : ↑(Icc a b)
n : ℕ
ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))
⊢ ↑t - ↑(addNSMul h δ n) ≤ ↑(projIcc a b h (a + (n + 1) • δ)) - ↑(addNSMul h δ n)

Tactic:
apply sub_le_sub_right

Result:
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
t : ↑(Icc a b)
n : ℕ
ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))
⊢ ↑t ≤ ↑(projIcc a b h (a + (n + 1) • δ))

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
t : ↑(Icc a b)
n : ℕ
ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))
⊢ |δ| ≤ δ

Tactic:
exact (abs_eq_self.mpr hδ).le

Result:
no goals
-- Mathlib/Analysis/Oscillation.lean
theorem oscillation_eq_zero [TopologicalSpace E] {f : E → F} {x : E} (hf : ContinuousAt f x) :
    oscillation f x = 0

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
x : E
hf : ContinuousAt f x
⊢ oscillation f x = 0

Tactic:
rw [← continuousWithinAt_univ f x] at hf

Result:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
x : E
hf : ContinuousWithinAt f univ x
⊢ oscillation f x = 0

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
x : E
hf : ContinuousWithinAt f univ x
⊢ oscillation f x = 0

Tactic:
exact oscillationWithin_univ_eq_oscillation f x ▸ hf.oscillationWithin_eq_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_neg_of_pos_of_neg {a b : Int} (ha : 0 < a) (hb : b < 0) : a * b < 0

Proof state:
a b : Int
ha : 0 < a
hb : b < 0
h : a * b < a * 0
⊢ a * b < 0

Tactic:
rwa [Int.mul_zero] at h

Result:
no goals

Proof state:
a b : Int
ha : 0 < a
hb : b < 0
⊢ a * b < 0

Tactic:
have h : a * b < a * 0 := Int.mul_lt_mul_of_pos_left hb ha

Result:
a b : Int
ha : 0 < a
hb : b < 0
h : a * b < a * 0
⊢ a * b < 0
-- Mathlib/Topology/Constructions.lean
theorem interior_prod_eq (s : Set X) (t : Set Y) : interior (s ×ˢ t) = interior s ×ˢ interior t :=
  ext fun ⟨a, b⟩ => by simp only [mem_interior_iff_mem_nhds, mem_prod, prod_mem_nhds_iff]

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
x✝ : X × Y
a : X
b : Y
⊢ (a, b) ∈ interior (s ×ˢ t) ↔ (a, b) ∈ interior s ×ˢ interior t

Tactic:
simp only [mem_interior_iff_mem_nhds, mem_prod, prod_mem_nhds_iff]

Result:
no goals