harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Submonoid/BigOperators.lean
theorem noncommProd_mem (S : Submonoid M) {ι : Type*} (t : Finset ι) (f : ι → M) (comm)
    (h : ∀ c ∈ t, f c ∈ S) : t.noncommProd f comm ∈ S

Proof state:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
⊢ t.noncommProd f comm ∈ S

Tactic:
apply multiset_noncommProd_mem

Result:
case h
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
⊢ ∀ x ∈ Multiset.map f t.val, x ∈ S

Proof state:
case h
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
y : M
⊢ y ∈ Multiset.map f t.val → y ∈ S

Tactic:
rw [Multiset.mem_map]

Result:
case h
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
y : M
⊢ (∃ a ∈ t.val, f a = y) → y ∈ S

Proof state:
case h
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
⊢ ∀ x ∈ Multiset.map f t.val, x ∈ S

Tactic:
intro y

Result:
case h
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
y : M
⊢ y ∈ Multiset.map f t.val → y ∈ S

Proof state:
case h.intro.intro
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
x : ι
hx : x ∈ t.val
⊢ f x ∈ S

Tactic:
exact h x hx

Result:
no goals

Proof state:
case h
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
y : M
⊢ (∃ a ∈ t.val, f a = y) → y ∈ S

Tactic:
rintro ⟨x, ⟨hx, rfl⟩⟩

Result:
case h.intro.intro
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
x : ι
hx : x ∈ t.val
⊢ f x ∈ S
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem pseudo_surjective_of_epi {P Q : C} (f : P ⟶ Q) [Epi f] : Function.Surjective f :=
  fun qbar =>
  Quotient.inductionOn qbar fun q =>
    ⟨(pullback.fst f q.hom : Over P),
      Quotient.sound <|
        ⟨pullback f q.hom, 𝟙 (pullback f q.hom), pullback.snd _ _, inferInstance, inferInstance, by
          rw [Category.id_comp, ← pullback.condition, app_hom, Over.coe_hom]⟩⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Epi f
qbar : Pseudoelement Q
q : Over Q
⊢ 𝟙 (pullback f q.hom) ≫ ((fun g => app f g) (Over.mk (pullback.fst f q.hom))).hom = pullback.snd f q.hom ≫ q.hom

Tactic:
rw [Category.id_comp, ← pullback.condition, app_hom, Over.coe_hom]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_two_neg : cos 2 < 0 :=
  calc cos 2 = cos (2 * 1) := congr_arg cos (mul_one _).symm
    _ = _ := Real.cos_two_mul 1
    _ ≤ 2 * (2 / 3) ^ 2 - 1

Proof state:
case h.h.ha

⊢ 0 ≤ cos 1

Tactic:
exact cos_one_pos.le

Result:
no goals

Proof state:
⊢ 2 * cos 1 ^ 2 - 1 ≤ 2 * (2 / 3) ^ 2 - 1

Tactic:
gcongr

Result:
case h.h.ha

⊢ 0 ≤ cos 1

case h.h.hab

⊢ cos 1 ≤ 2 / 3

Proof state:
case h.h.hab

⊢ cos 1 ≤ 2 / 3

Tactic:
apply cos_one_le

Result:
no goals

Proof state:
⊢ 2 * (2 / 3) ^ 2 - 1 < 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_append_length_eq (l l' : List α) : (l ++ l').rotate l.length = l' ++ l

Proof state:
α : Type u
l l' : List α
⊢ (l ++ l').rotate l.length = l' ++ l

Tactic:
rw [rotate_eq_rotate']

Result:
α : Type u
l l' : List α
⊢ (l ++ l').rotate' l.length = l' ++ l

Proof state:
case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l' : List α), (tail✝ ++ l').rotate' tail✝.length = l' ++ tail✝
l' : List α
⊢ (head✝ :: tail✝ ++ l').rotate' (head✝ :: tail✝).length = l' ++ head✝ :: tail✝

Tactic:
simp_all [rotate']

Result:
no goals

Proof state:
case nil
α : Type u
l' : List α
⊢ ([] ++ l').rotate' [].length = l' ++ []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l l' : List α
⊢ (l ++ l').rotate' l.length = l' ++ l

Tactic:
induction l generalizing l'

Result:
case nil
α : Type u
l' : List α
⊢ ([] ++ l').rotate' [].length = l' ++ []

case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l' : List α), (tail✝ ++ l').rotate' tail✝.length = l' ++ tail✝
l' : List α
⊢ (head✝ :: tail✝ ++ l').rotate' (head✝ :: tail✝).length = l' ++ head✝ :: tail✝
-- Mathlib/Probability/Distributions/Gaussian.lean
lemma gaussianPDFReal_sub {μ : ℝ} {v : ℝ≥0} (x y : ℝ) :
    gaussianPDFReal μ v (x - y) = gaussianPDFReal (μ + y) v x

Proof state:
μ : ℝ
v : ℝ≥0
x y : ℝ
⊢ (√(2 * π * ↑v))⁻¹ * rexp (-(x - y - μ) ^ 2 / (2 * ↑v)) = (√(2 * π * ↑v))⁻¹ * rexp (-(x - (μ + y)) ^ 2 / (2 * ↑v))

Tactic:
rw [sub_add_eq_sub_sub_swap]

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
x y : ℝ
⊢ gaussianPDFReal μ v (x - y) = gaussianPDFReal (μ + y) v x

Tactic:
simp only [gaussianPDFReal]

Result:
μ : ℝ
v : ℝ≥0
x y : ℝ
⊢ (√(2 * π * ↑v))⁻¹ * rexp (-(x - y - μ) ^ 2 / (2 * ↑v)) = (√(2 * π * ↑v))⁻¹ * rexp (-(x - (μ + y)) ^ 2 / (2 * ↑v))
-- Mathlib/Analysis/Analytic/Inverse.lean
theorem leftInv_removeZero (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
    p.removeZero.leftInv i x = p.leftInv i x

Proof state:
case mk.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
c : Composition (n + 2)
hc : c.length < n + 2
cuniv : ⟨c, hc⟩ ∈ univ
v : Fin (n + 2) → F
⊢ (ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap ↑i.symm) (↑⟨c, hc⟩)
        (p.removeZero.leftInv i x (↑⟨c, hc⟩).length))
      v =
    (ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap ↑i.symm) (↑⟨c, hc⟩)
        (p.leftInv i x (↑⟨c, hc⟩).length))
      v

Tactic:
dsimp

Result:
case mk.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
c : Composition (n + 2)
hc : c.length < n + 2
cuniv : ⟨c, hc⟩ ∈ univ
v : Fin (n + 2) → F
⊢ (p.removeZero.leftInv i x c.length) ((p.removeZero.compContinuousLinearMap ↑i.symm).applyComposition c v) =
    (p.leftInv i x c.length) ((p.compContinuousLinearMap ↑i.symm).applyComposition c v)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n : ℕ
IH : ∀ m < 1, p.removeZero.leftInv i x m = p.leftInv i x m
⊢ p.removeZero.leftInv i x 1 = p.leftInv i x 1

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
⊢ p.removeZero.leftInv i x (n + 2) = p.leftInv i x (n + 2)

Tactic:
simp only [leftInv, neg_inj]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
⊢ ∑ c : { c // c.length < n + 2 },
      ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap ↑i.symm) (↑c)
        (p.removeZero.leftInv i x (↑c).length) =
    ∑ c : { c // c.length < n + 2 },
      ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap ↑i.symm) (↑c) (p.leftInv i x (↑c).length)
-- Mathlib/Data/ENNReal/Order.lean
theorem lt_top_of_mul_ne_top_right (h : a * b ≠ ∞) (ha : a ≠ 0) : b < ∞ :=
  lt_top_of_mul_ne_top_left (by rwa [mul_comm]) ha

Proof state:
a b : ℝ≥0∞
h : a * b ≠ ⊤
ha : a ≠ 0
⊢ b * a ≠ ⊤

Tactic:
rwa [mul_comm]

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
theorem singleton_disjoint {l : Multiset α} {a : α} : Disjoint {a} l ↔ a ∉ l

Proof state:
α : Type u_1
l : Multiset α
a : α
⊢ _root_.Disjoint {a} l ↔ a ∉ l

Tactic:
simp [disjoint_left]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean
theorem exists_lt_lowerSemicontinuous_lintegral_ge [SigmaFinite μ] (f : α → ℝ≥0)
    (fmeas : Measurable f) {ε : ℝ≥0∞} (ε0 : ε ≠ 0) :
    ∃ g : α → ℝ≥0∞,
      (∀ x, (f x : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ (∫⁻ x, g x ∂μ) ≤ (∫⁻ x, f x ∂μ) + ε

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), ↑(w x) ∂μ < ε / 2
f' : α → ℝ≥0∞ := fun x => ↑(f x + w x)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
⊢ ∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε

Tactic:
refine ⟨g, fun x => ?_, gcont, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), ↑(w x) ∂μ < ε / 2
f' : α → ℝ≥0∞ := fun x => ↑(f x + w x)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
x : α
⊢ ↑(f x) < g x

case intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), ↑(w x) ∂μ < ε / 2
f' : α → ℝ≥0∞ := fun x => ↑(f x + w x)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), ↑(w x) ∂μ < ε / 2
f' : α → ℝ≥0∞ := fun x => ↑(f x + w x)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
x : α
⊢ ↑(f x) < f' x

Tactic:
simpa only [← ENNReal.coe_lt_coe, add_zero] using add_lt_add_left (wpos x) (f x)

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem mkAlgHom_coe (s : A → A → Prop) : (mkAlgHom S s : A →+* RingQuot s) = mkRingHom s

Proof state:
S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
⊢ ↑{ toFun := fun x => { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
        commutes' := ⋯ } =
    { toFun := fun x => { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Tactic:
rfl

Result:
no goals

Proof state:
S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
⊢ ↑(mkAlgHom S s) = mkRingHom s

Tactic:
simp_rw [mkAlgHom_def, mkRingHom_def]

Result:
S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
⊢ ↑{ toFun := fun x => { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
        commutes' := ⋯ } =
    { toFun := fun x => { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib/Analysis/Normed/Module/Basic.lean
theorem NormedSpace.exists_lt_norm (c : ℝ) : ∃ x : E, c < ‖x‖

Proof state:
case intro
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
⊢ ∃ x, c < ‖x‖

Tactic:
rcases NormedField.exists_lt_norm 𝕜 (c / ‖x‖) with ⟨r, hr⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ ∃ x, c < ‖x‖

Proof state:
case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ 0 < ‖x‖

Tactic:
rwa [norm_pos_iff]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
⊢ ∃ x, c < ‖x‖

Tactic:
rcases exists_ne (0 : E) with ⟨x, hx⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
⊢ ∃ x, c < ‖x‖

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ ∃ x, c < ‖x‖

Tactic:
use r • x

Result:
case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ c < ‖r • x‖

Proof state:
case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ c < ‖r • x‖

Tactic:
rwa [norm_smul, ← div_lt_iff₀]

Result:
case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ 0 < ‖x‖
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {fallback v : β} :
    getD (m.insertIfNew k v) a fallback =
      if k == a ∧ ¬k ∈ m then v else getD m a fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
fallback v : β
⊢ getD (m.insertIfNew k v) a fallback = if (k == a) = true ∧ m.contains k = false then v else getD m a fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_insertIfNew

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
fallback v : β
⊢ getD (m.insertIfNew k v) a fallback = if (k == a) = true ∧ ¬k ∈ m then v else getD m a fallback

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
fallback v : β
⊢ getD (m.insertIfNew k v) a fallback = if (k == a) = true ∧ m.contains k = false then v else getD m a fallback
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma mapHomologicalComplexXIso_eq (n m : ℤ) (hnm : n + 1 = m) :
    mapHomologicalComplexXIso φ H n = mapHomologicalComplexXIso' φ H n m hnm

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ mapHomologicalComplexXIso φ H n = mapHomologicalComplexXIso' φ H n (n + 1) ⋯

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n m : ℤ
hnm : n + 1 = m
⊢ mapHomologicalComplexXIso φ H n = mapHomologicalComplexXIso' φ H n m hnm

Tactic:
subst hnm

Result:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ mapHomologicalComplexXIso φ H n = mapHomologicalComplexXIso' φ H n (n + 1) ⋯
-- Mathlib/Data/Nat/Bits.lean
@[simp]
lemma bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n)

Proof state:
n : ℕ
⊢ n.succ.bodd = !n.bodd

Tactic:
simp only [bodd, boddDiv2]

Result:
n : ℕ
⊢ (match n.boddDiv2 with
      | (false, m) => (true, m)
      | (true, m) => (false, m.succ)).fst =
    !n.boddDiv2.fst

Proof state:
n : ℕ
⊢ (match n.boddDiv2 with
      | (false, m) => (true, m)
      | (true, m) => (false, m.succ)).fst =
    !n.boddDiv2.fst

Tactic:
let ⟨b,m⟩ := boddDiv2 n

Result:
n : ℕ
b : Bool
m : ℕ
⊢ (match (b, m) with
      | (false, m) => (true, m)
      | (true, m) => (false, m.succ)).fst =
    !(b, m).fst

Proof state:
n : ℕ
b : Bool
m : ℕ
⊢ (match (b, m) with
      | (false, m) => (true, m)
      | (true, m) => (false, m.succ)).fst =
    !(b, m).fst

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/RingTheory/Derivation/Basic.lean
@[simp]
lemma liftOfRightInverse_apply {f : F} {f_inv : M → A} (hf : Function.RightInverse f_inv f)
    {d : Derivation R A A} (hd : ∀ x, f x = 0 → f (d x) = 0) (x : A) :
    Derivation.liftOfRightInverse hf hd (f x) = f (d x)

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : A
⊢ f (d (f_inv (f x) - x)) = 0

Tactic:
apply hd

Result:
case a
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : A
⊢ f (f_inv (f x) - x) = 0

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : A
⊢ (liftOfRightInverse hf hd) (f x) = f (d x)

Tactic:
suffices f (d (f_inv (f x) - x)) = 0 by simpa [sub_eq_zero]

Result:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : A
⊢ f (d (f_inv (f x) - x)) = 0

Proof state:
case a
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : A
⊢ f (f_inv (f x) - x) = 0

Tactic:
simp [hf _]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : A
this : f (d (f_inv (f x) - x)) = 0
⊢ (liftOfRightInverse hf hd) (f x) = f (d x)

Tactic:
simpa [sub_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem map_comap_eq (hf : N₂ ≤ f.range) : map f (comap f N₂) = N₂

Proof state:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L M₂
N₂ : LieSubmodule R L M₂
f : M →ₗ⁅R,L⁆ M₂
hf : N₂ ≤ f.range
⊢ ↑(map f (comap f N₂)) = ↑N₂

Tactic:
exact Set.image_preimage_eq_of_subset hf

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L M₂
N₂ : LieSubmodule R L M₂
f : M →ₗ⁅R,L⁆ M₂
hf : N₂ ≤ f.range
⊢ map f (comap f N₂) = N₂

Tactic:
rw [SetLike.ext'_iff]

Result:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L M₂
N₂ : LieSubmodule R L M₂
f : M →ₗ⁅R,L⁆ M₂
hf : N₂ ≤ f.range
⊢ ↑(map f (comap f N₂)) = ↑N₂
-- Mathlib/Computability/Primrec.lean
theorem map_decode_iff {f : α → β → σ} :
    (Primrec₂ fun a n => (@decode β _ n).map (f a)) ↔ Primrec₂ f

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec₂ fun a n => Option.map (f a) (decode n)) ↔ Primrec₂ f

Tactic:
simp only [Option.map_eq_bind]

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec₂ fun a n => (decode n).bind (some ∘ f a)) ↔ Primrec₂ f

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec₂ fun a n => (decode n).bind (some ∘ f a)) ↔ Primrec₂ f

Tactic:
exact bind_decode_iff.trans Primrec₂.option_some_iff

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem map_div_atTop_eq_nat (k : ℕ) (hk : 0 < k) : map (fun a => a / k) atTop = atTop :=
  map_atTop_eq_of_gc (fun b => k * b + (k - 1)) 1 (fun _ _ h => Nat.div_le_div_right h)
    -- Porting note: there was a parse error in `calc`, use `simp` instead
    (fun a b _ => by rw [Nat.div_le_iff_le_mul_add_pred hk])
    fun b _ => by rw [Nat.mul_add_div hk, Nat.div_eq_of_lt, add_zero]; omega

Proof state:
k : ℕ
hk : 0 < k
a b : ℕ
x✝ : b ≥ 1
⊢ a / k ≤ b ↔ a ≤ (fun b => k * b + (k - 1)) b

Tactic:
rw [Nat.div_le_iff_le_mul_add_pred hk]

Result:
no goals

Proof state:
k : ℕ
hk : 0 < k
b : ℕ
x✝ : b ≥ 1
⊢ k - 1 < k

Tactic:
omega

Result:
no goals

Proof state:
k : ℕ
hk : 0 < k
b : ℕ
x✝ : b ≥ 1
⊢ b ≤ (fun b => k * b + (k - 1)) b / k

Tactic:
rw [Nat.mul_add_div hk, Nat.div_eq_of_lt, add_zero]

Result:
k : ℕ
hk : 0 < k
b : ℕ
x✝ : b ≥ 1
⊢ k - 1 < k