harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma div_nonpos_of_nonpos_of_nonneg [MulPosMono G₀] (ha : a ≤ 0) (hb : 0 ≤ b) : a / b ≤ 0

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : MulPosMono G₀
ha : a ≤ 0
hb : 0 ≤ b
⊢ a / b ≤ 0

Tactic:
rw [div_eq_mul_inv]

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : MulPosMono G₀
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b⁻¹ ≤ 0

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : MulPosMono G₀
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b⁻¹ ≤ 0

Tactic:
exact mul_nonpos_of_nonpos_of_nonneg ha (inv_nonneg.2 hb)

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Defs.lean
theorem mul_self_le_one_iff : a * a ≤ 1 ↔ a ≤ 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommMonoid α
a : α
⊢ a * a ≤ 1 ↔ a ≤ 1

Tactic:
simp [← not_iff_not]

Result:
no goals
-- Mathlib/Topology/Algebra/Support.lean
theorem HasCompactSupport.smul_right (hf : HasCompactSupport f) : HasCompactSupport (f • f')

Proof state:
α : Type u_2
M : Type u_7
R : Type u_8
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0

Tactic:
exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]

Result:
no goals

Proof state:
α : Type u_2
M : Type u_7
R : Type u_8
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
hf : HasCompactSupport f
⊢ HasCompactSupport (f • f')

Tactic:
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢

Result:
α : Type u_2
M : Type u_7
R : Type u_8
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0

Proof state:
α : Type u_2
M : Type u_7
R : Type u_8
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ (f • f') x = 0 x

Tactic:
simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attach_congr {l₁ l₂ : Vector α n} (h : l₁ = l₂) :
    l₁.attach = l₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩)

Proof state:
α : Type u_1
n : Nat
l₁ l₂ : Vector α n
h : l₁ = l₂
⊢ l₁.attach = map (fun x => ⟨x.val, ⋯⟩) l₂.attach

Tactic:
subst h

Result:
α : Type u_1
n : Nat
l₁ : Vector α n
⊢ l₁.attach = map (fun x => ⟨x.val, ⋯⟩) l₁.attach

Proof state:
α : Type u_1
n : Nat
l₁ : Vector α n
⊢ l₁.attach = map (fun x => ⟨x.val, ⋯⟩) l₁.attach

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem of_nat {n : ℕ} : padicValInt p n = padicValNat p n

Proof state:
p n : ℕ
⊢ padicValInt p ↑n = padicValNat p n

Tactic:
simp [padicValInt]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_mul {p q : R[X]} (hpq : p * q ≠ 0) : (p * q).roots = p.roots + q.roots

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p * q ≠ 0
⊢ (p * q).roots = p.roots + q.roots

Tactic:
exact Multiset.ext.mpr fun r => by
  rw [count_add, count_roots, count_roots, count_roots, rootMultiplicity_mul hpq]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p * q ≠ 0
⊢ (p * q).roots = p.roots + q.roots

Tactic:
classical
exact Multiset.ext.mpr fun r => by
  rw [count_add, count_roots, count_roots, count_roots, rootMultiplicity_mul hpq]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p * q ≠ 0
r : R
⊢ count r (p * q).roots = count r (p.roots + q.roots)

Tactic:
rw [count_add, count_roots, count_roots, count_roots, rootMultiplicity_mul hpq]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Span.lean
theorem toSpanSingleton_homothety (x : E) (c : 𝕜) :
    ‖LinearMap.toSpanSingleton 𝕜 E x c‖ = ‖x‖ * ‖c‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
x : E
c : 𝕜
⊢ ‖(toSpanSingleton 𝕜 E x) c‖ = ‖x‖ * ‖c‖

Tactic:
rw [mul_comm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
x : E
c : 𝕜
⊢ ‖(toSpanSingleton 𝕜 E x) c‖ = ‖c‖ * ‖x‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
x : E
c : 𝕜
⊢ ‖(toSpanSingleton 𝕜 E x) c‖ = ‖c‖ * ‖x‖

Tactic:
exact norm_smul _ _

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem toList_node : (.node c a x b : RBNode α).toList = a.toList ++ x :: b.toList

Proof state:
α : Type u_1
c : RBColor
a : RBNode α
x : α
b : RBNode α
⊢ a.toList ++ x :: foldr (fun x1 x2 => x1 :: x2) b [] = a.toList ++ x :: b.toList

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
c : RBColor
a : RBNode α
x : α
b : RBNode α
⊢ (node c a x b).toList = a.toList ++ x :: b.toList

Tactic:
rw [toList, foldr, foldr_cons]

Result:
α : Type u_1
c : RBColor
a : RBNode α
x : α
b : RBNode α
⊢ a.toList ++ x :: foldr (fun x1 x2 => x1 :: x2) b [] = a.toList ++ x :: b.toList
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem nhdsLT_eq_bot_iff {a : α} : 𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a

Proof state:
case h.e'_2.h.e'_2.h.e'_2.h.h.a
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
e_1✝ : α = αᵒᵈ
x✝ : α
⊢ x✝ ⋖ a ↔ toDual a ⋖ x✝

Tactic:
exact ofDual_covBy_ofDual_iff

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a

Tactic:
convert (config := { preTransparency := .default }) nhdsGT_eq_bot_iff (a := OrderDual.toDual a)
  using 4

Result:
case h.e'_2.h.e'_2.h.e'_2.h.h.a
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
e_1✝ : α = αᵒᵈ
x✝ : α
⊢ x✝ ⋖ a ↔ toDual a ⋖ x✝
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfpBFamily_le_apply (ho : o ≠ 0) (H : ∀ i hi, IsNormal (f i hi)) {a b} :
    (∃ i hi, nfpBFamily.{u, v} o f a ≤ f i hi b) ↔ nfpBFamily.{u, v} o f a ≤ b

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < o.nfpBFamily f a) ↔ b < o.nfpBFamily f a

Tactic:
exact apply_lt_nfpBFamily_iff.{u, v} ho H

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
⊢ (¬∃ i, ∃ (hi : i < o), o.nfpBFamily f a ≤ f i hi b) ↔ ¬o.nfpBFamily f a ≤ b

Tactic:
push_neg

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < o.nfpBFamily f a) ↔ b < o.nfpBFamily f a

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
⊢ (∃ i, ∃ (hi : i < o), o.nfpBFamily f a ≤ f i hi b) ↔ o.nfpBFamily f a ≤ b

Tactic:
rw [← not_iff_not]

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
⊢ (¬∃ i, ∃ (hi : i < o), o.nfpBFamily f a ≤ f i hi b) ↔ ¬o.nfpBFamily f a ≤ b
-- Mathlib/Data/Stream/Init.lean
lemma get_append_left (h : n < x.length) : (x ++ₛ a).get n = x[n]

Proof state:
case cons
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
n : ℕ
h : n < (b :: x).length
⊢ (b :: x ++ₛ a).get n = (b :: x)[n]

Tactic:
rcases n with (_ | n)

Result:
case cons.zero
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
h : 0 < (b :: x).length
⊢ (b :: x ++ₛ a).get 0 = (b :: x)[0]

case cons.succ
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
n : ℕ
h : n + 1 < (b :: x).length
⊢ (b :: x ++ₛ a).get (n + 1) = (b :: x)[n + 1]

Proof state:
case nil
α : Type u
a : Stream' α
n : ℕ
h : n < [].length
⊢ ([] ++ₛ a).get n = [][n]

Tactic:
simp at h

Result:
no goals

Proof state:
case cons.zero
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
h : 0 < (b :: x).length
⊢ (b :: x ++ₛ a).get 0 = (b :: x)[0]

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
n : ℕ
h : n + 1 < (b :: x).length
⊢ (b :: x ++ₛ a).get (n + 1) = (b :: x)[n + 1]

Tactic:
simp [ih n (by simpa using h), cons_append_stream]

Result:
no goals

Proof state:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n < x.length
⊢ (x ++ₛ a).get n = x[n]

Tactic:
induction' x with b x ih generalizing n

Result:
case nil
α : Type u
a : Stream' α
n : ℕ
h : n < [].length
⊢ ([] ++ₛ a).get n = [][n]

case cons
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
n : ℕ
h : n < (b :: x).length
⊢ (b :: x ++ₛ a).get n = (b :: x)[n]

Proof state:
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
n : ℕ
h : n + 1 < (b :: x).length
⊢ n < x.length

Tactic:
simpa using h

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem ofReal_setIntegral_one_of_measure_ne_top {X : Type*} {m : MeasurableSpace X}
    {μ : Measure X} {s : Set X} (hs : μ s ≠ ∞) : ENNReal.ofReal (∫ _ in s, (1 : ℝ) ∂μ) = μ s :=
  calc
    ENNReal.ofReal (∫ _ in s, (1 : ℝ) ∂μ) = ENNReal.ofReal (∫ _ in s, ‖(1 : ℝ)‖ ∂μ)

Proof state:
X : Type u_5
m : MeasurableSpace X
μ : Measure X
s : Set X
hs : μ s ≠ ⊤
⊢ ENNReal.ofReal (∫ (x : X) in s, 1 ∂μ) = ENNReal.ofReal (∫ (x : X) in s, ‖1‖ ∂μ)

Tactic:
simp only [norm_one]

Result:
no goals

Proof state:
X : Type u_5
m : MeasurableSpace X
μ : Measure X
s : Set X
hs : μ s ≠ ⊤
⊢ ENNReal.ofReal (∫ (x : X) in s, ‖1‖ ∂μ) = ∫⁻ (x : X) in s, 1 ∂μ

Tactic:
simpa [ofReal_integral_norm_eq_lintegral_enorm (integrableOn_const.2 (.inr hs.lt_top))]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombination_filter_of_ne (w : ι → k) (p : ι → P) {pred : ι → Prop}
    [DecidablePred pred] (h : ∀ i ∈ s, w i ≠ 0 → pred i) :
    {x ∈ s | pred x}.affineCombination k p w = s.affineCombination k p w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
⊢ (affineCombination k (filter (fun x => pred x) s) p) w = (affineCombination k s p) w

Tactic:
rw [affineCombination_apply, affineCombination_apply,
  s.weightedVSubOfPoint_filter_of_ne _ _ _ h]

Result:
no goals
-- Mathlib/Algebra/Module/Torsion.lean
theorem coe_torsion_eq_annihilator_ne_bot :
    (torsion R M : Set M) = { x : M | (R ∙ x).annihilator ≠ ⊥ }

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | ∃ x_1, (∀ (n : M), (∃ a, a • x = n) → x_1 • n = 0) ∧ x_1 ≠ 0}

Tactic:
exact
  ⟨fun ⟨a, hax⟩ =>
    ⟨a, fun _ ⟨b, hb⟩ => by rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero],
      nonZeroDivisors.coe_ne_zero _⟩,
    fun ⟨a, hax, ha⟩ => ⟨⟨_, mem_nonZeroDivisors_of_ne_zero ha⟩, hax x ⟨1, one_smul _ _⟩⟩⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
x✝² : x ∈ ↑(torsion R M)
a : ↥R⁰
hax : a • x = 0
x✝¹ : M
x✝ : ∃ a, a • x = x✝¹
b : R
hb : b • x = x✝¹
⊢ ↑a • x✝¹ = 0

Tactic:
rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ ↑(torsion R M) = {x | (span R {x}).annihilator ≠ ⊥}

Tactic:
ext x

Result:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | (span R {x}).annihilator ≠ ⊥}

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | (span R {x}).annihilator ≠ ⊥}

Tactic:
simp_rw [Submodule.ne_bot_iff, mem_annihilator, mem_span_singleton]

Result:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | ∃ x_1, (∀ (n : M), (∃ a, a • x = n) → x_1 • n = 0) ∧ x_1 ≠ 0}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem mem_attachWith (l : List α) {q : α → Prop} (H) (x : {x // q x}) :
    x ∈ l.attachWith q H ↔ x.1 ∈ l

Proof state:
case cons.mpr.inl
α : Type u_1
q : α → Prop
x : { x // q x }
a : α
l : List α
ih : ∀ (H : ∀ (x : α), x ∈ l → q x), x ∈ l.attachWith q H ↔ x.val ∈ l
H : ∀ (x : α), x ∈ a :: l → q x
h : x.val = a
⊢ x = ⟨a, ⋯⟩ ∨ x.val ∈ l

Tactic:
simp [← h]

Result:
no goals

Proof state:
case cons
α : Type u_1
q : α → Prop
x : { x // q x }
a : α
l : List α
ih : ∀ (H : ∀ (x : α), x ∈ l → q x), x ∈ l.attachWith q H ↔ x.val ∈ l
H : ∀ (x : α), x ∈ a :: l → q x
⊢ x ∈ (a :: l).attachWith q H ↔ x.val ∈ a :: l

Tactic:
simp [ih]

Result:
case cons
α : Type u_1
q : α → Prop
x : { x // q x }
a : α
l : List α
ih : ∀ (H : ∀ (x : α), x ∈ l → q x), x ∈ l.attachWith q H ↔ x.val ∈ l
H : ∀ (x : α), x ∈ a :: l → q x
⊢ x = ⟨a, ⋯⟩ ∨ x.val ∈ l ↔ x.val = a ∨ x.val ∈ l

Proof state:
case cons.mpr
α : Type u_1
q : α → Prop
x : { x // q x }
a : α
l : List α
ih : ∀ (H : ∀ (x : α), x ∈ l → q x), x ∈ l.attachWith q H ↔ x.val ∈ l
H : ∀ (x : α), x ∈ a :: l → q x
⊢ x.val = a ∨ x.val ∈ l → x = ⟨a, ⋯⟩ ∨ x.val ∈ l

Tactic:
rintro (h | h)

Result:
case cons.mpr.inl
α : Type u_1
q : α → Prop
x : { x // q x }
a : α
l : List α
ih : ∀ (H : ∀ (x : α), x ∈ l → q x), x ∈ l.attachWith q H ↔ x.val ∈ l
H : ∀ (x : α), x ∈ a :: l → q x
h : x.val = a
⊢ x = ⟨a, ⋯⟩ ∨ x.val ∈ l

case cons.mpr.inr
α : Type u_1
q : α → Prop
x : { x // q x }
a : α
l : List α
ih : ∀ (H : ∀ (x : α), x ∈ l → q x), x ∈ l.attachWith q H ↔ x.val ∈ l
H : ∀ (x : α), x ∈ a :: l → q x
h : x.val ∈ l
⊢ x = ⟨a, ⋯⟩ ∨ x.val ∈ l

Proof state:
case cons
α : Type u_1
q : α → Prop
x : { x // q x }
a : α
l : List α
ih : ∀ (H : ∀ (x : α), x ∈ l → q x), x ∈ l.attachWith q H ↔ x.val ∈ l
H : ∀ (x : α), x ∈ a :: l → q x
⊢ x = ⟨a, ⋯⟩ ∨ x.val ∈ l ↔ x.val = a ∨ x.val ∈ l

Tactic:
constructor

Result:
case cons.mp
α : Type u_1
q : α → Prop
x : { x // q x }
a : α
l : List α
ih : ∀ (H : ∀ (x : α), x ∈ l → q x), x ∈ l.attachWith q H ↔ x.val ∈ l
H : ∀ (x : α), x ∈ a :: l → q x
⊢ x = ⟨a, ⋯⟩ ∨ x.val ∈ l → x.val = a ∨ x.val ∈ l

case cons.mpr
α : Type u_1
q : α → Prop
x : { x // q x }
a : α
l : List α
ih : ∀ (H : ∀ (x : α), x ∈ l → q x), x ∈ l.attachWith q H ↔ x.val ∈ l
H : ∀ (x : α), x ∈ a :: l → q x
⊢ x.val = a ∨ x.val ∈ l → x = ⟨a, ⋯⟩ ∨ x.val ∈ l

Proof state:
case cons.mpr.inr
α : Type u_1
q : α → Prop
x : { x // q x }
a : α
l : List α
ih : ∀ (H : ∀ (x : α), x ∈ l → q x), x ∈ l.attachWith q H ↔ x.val ∈ l
H : ∀ (x : α), x ∈ a :: l → q x
h : x.val ∈ l
⊢ x = ⟨a, ⋯⟩ ∨ x.val ∈ l

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.mp
α : Type u_1
q : α → Prop
x : { x // q x }
a : α
l : List α
ih : ∀ (H : ∀ (x : α), x ∈ l → q x), x ∈ l.attachWith q H ↔ x.val ∈ l
H : ∀ (x : α), x ∈ a :: l → q x
⊢ x = ⟨a, ⋯⟩ ∨ x.val ∈ l → x.val = a ∨ x.val ∈ l

Tactic:
rintro (_ | _) <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
q : α → Prop
x : { x // q x }
H : ∀ (x : α), x ∈ [] → q x
⊢ x ∈ [].attachWith q H ↔ x.val ∈ []

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem ext_of_forall_lintegral_eq [HasOuterApproxClosed Ω] [BorelSpace Ω]
    {μ ν : FiniteMeasure Ω} (h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ x, f x ∂μ = ∫⁻ x, f x ∂ν) :
    μ = ν

Proof state:
case a
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν
⊢ ↑μ = ↑ν

Tactic:
exact ext_of_forall_lintegral_eq_of_IsFiniteMeasure h

Result:
no goals

Proof state:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν
⊢ μ = ν

Tactic:
apply Subtype.ext

Result:
case a
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν
⊢ ↑μ = ↑ν
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem combine_sat : (c : Constraint) → (c' : Constraint) → (t : Int) →
    (c.combine c').sat t = (c.sat t ∧ c'.sat t)

Proof state:
case mk.some.some.mk.some.none
l₁ u₁ l₂ t : Int
⊢ (l₁ ≤ t ∧ l₂ ≤ t) ∧ t ≤ u₁ ↔ (l₁ ≤ t ∧ t ≤ u₁) ∧ l₂ ≤ t

Tactic:
rw [and_assoc, and_assoc, And.comm (a := l₂ ≤ t)]

Result:
no goals

Proof state:
case mk.none.some.mk.some.some
u₁ l₂ u₂ t : Int
⊢ l₂ ≤ t ∧ t ≤ u₁ ∧ t ≤ u₂ ↔ t ≤ u₁ ∧ l₂ ≤ t ∧ t ≤ u₂

Tactic:
rw [← and_assoc, And.comm (a := l₂ ≤ t), and_assoc]

Result:
no goals

Proof state:
case mk.some.some.mk.some.some
l₁ u₁ l₂ u₂ t : Int
⊢ (l₁ ≤ t ∧ l₂ ≤ t) ∧ t ≤ u₁ ∧ t ≤ u₂ ↔ (l₁ ≤ t ∧ t ≤ u₁) ∧ l₂ ≤ t ∧ t ≤ u₂

Tactic:
rw [and_assoc, ← and_assoc (a := l₂ ≤ t), And.comm (a := l₂ ≤ t), and_assoc, and_assoc]

Result:
no goals

Proof state:
case mk.some.none.mk.some.some
l₁ l₂ u₂ t : Int
⊢ (l₁ ≤ t ∧ l₂ ≤ t) ∧ t ≤ u₂ ↔ l₁ ≤ t ∧ l₂ ≤ t ∧ t ≤ u₂

Tactic:
rw [and_assoc]

Result:
no goals

Proof state:
case mk.none.some.mk.some.none
u₁ l₂ t : Int
⊢ l₂ ≤ t ∧ t ≤ u₁ ↔ t ≤ u₁ ∧ l₂ ≤ t

Tactic:
rw [And.comm]

Result:
no goals

Proof state:
case mk.some.some.mk.none.some
l₁ u₁ u₂ t : Int
⊢ l₁ ≤ t ∧ t ≤ u₁ ∧ t ≤ u₂ ↔ (l₁ ≤ t ∧ t ≤ u₁) ∧ t ≤ u₂

Tactic:
rw [and_assoc]

Result:
no goals

Proof state:
⊢ ∀ (c c' : Constraint) (t : Int), ((c.combine c').sat t = true) = (c.sat t = true ∧ c'.sat t = true)

Tactic:
rintro ⟨_ | l₁, _ | u₁⟩ <;> rintro ⟨_ | l₂, _ | u₂⟩ t
  <;> simp [sat, LowerBound.sat, UpperBound.sat, combine, Int.le_min, Int.max_le] at *

Result:
case mk.none.some.mk.some.none
u₁ l₂ t : Int
⊢ l₂ ≤ t ∧ t ≤ u₁ ↔ t ≤ u₁ ∧ l₂ ≤ t

case mk.none.some.mk.some.some
u₁ l₂ u₂ t : Int
⊢ l₂ ≤ t ∧ t ≤ u₁ ∧ t ≤ u₂ ↔ t ≤ u₁ ∧ l₂ ≤ t ∧ t ≤ u₂

case mk.some.none.mk.some.some
l₁ l₂ u₂ t : Int
⊢ (l₁ ≤ t ∧ l₂ ≤ t) ∧ t ≤ u₂ ↔ l₁ ≤ t ∧ l₂ ≤ t ∧ t ≤ u₂

case mk.some.some.mk.none.some
l₁ u₁ u₂ t : Int
⊢ l₁ ≤ t ∧ t ≤ u₁ ∧ t ≤ u₂ ↔ (l₁ ≤ t ∧ t ≤ u₁) ∧ t ≤ u₂

case mk.some.some.mk.some.none
l₁ u₁ l₂ t : Int
⊢ (l₁ ≤ t ∧ l₂ ≤ t) ∧ t ≤ u₁ ↔ (l₁ ≤ t ∧ t ≤ u₁) ∧ l₂ ≤ t

case mk.some.some.mk.some.some
l₁ u₁ l₂ u₂ t : Int
⊢ (l₁ ≤ t ∧ l₂ ≤ t) ∧ t ≤ u₁ ∧ t ≤ u₂ ↔ (l₁ ≤ t ∧ t ≤ u₁) ∧ l₂ ≤ t ∧ t ≤ u₂
-- Mathlib/Order/SuccPred/Basic.lean
theorem succ_lt_succ_iff : succ a < succ b ↔ a < b

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ succ a < succ b ↔ a < b

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Lemmas.lean
lemma lipschitzWith_sub : LipschitzWith 2 (fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 - p.2)

Proof state:
this : Isometry (Prod.map toReal toReal)
⊢ LipschitzWith 2 (Subtype.val ∘ fun p => p.1 - p.2)

Tactic:
convert (((LipschitzWith.prod_fst.comp this.lipschitz).sub
  (LipschitzWith.prod_snd.comp this.lipschitz)).max_const 0)

Result:
case h.e'_5
this : Isometry (Prod.map toReal toReal)
⊢ 2 = 1 * 1 + 1 * 1

Proof state:
⊢ LipschitzWith 2 (Subtype.val ∘ fun p => p.1 - p.2)

Tactic:
have : Isometry (Prod.map ((↑) : ℝ≥0 → ℝ) ((↑) : ℝ≥0 → ℝ)) :=
  isometry_subtype_coe.prod_map isometry_subtype_coe

Result:
this : Isometry (Prod.map toReal toReal)
⊢ LipschitzWith 2 (Subtype.val ∘ fun p => p.1 - p.2)

Proof state:
case h.e'_5
this : Isometry (Prod.map toReal toReal)
⊢ 2 = 1 * 1 + 1 * 1

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ LipschitzWith 2 fun p => p.1 - p.2

Tactic:
rw [← isometry_subtype_coe.lipschitzWith_iff]

Result:
⊢ LipschitzWith 2 (Subtype.val ∘ fun p => p.1 - p.2)
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem DifferentiableWithinAt.hasGradientWithinAt (h : DifferentiableWithinAt 𝕜 f s x) :
    HasGradientWithinAt f (gradientWithin f s x) s x

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
s : Set F
h : DifferentiableWithinAt 𝕜 f s x
⊢ HasGradientWithinAt f (gradientWithin f s x) s x

Tactic:
rw [hasGradientWithinAt_iff_hasFDerivWithinAt, gradientWithin,
  (toDual 𝕜 F).apply_symm_apply (fderivWithin 𝕜 f s x)]

Result:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
s : Set F
h : DifferentiableWithinAt 𝕜 f s x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
s : Set F
h : DifferentiableWithinAt 𝕜 f s x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x

Tactic:
exact h.hasFDerivWithinAt

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Hom.lean
theorem hom_chart (y₀ y : LE₁E₂) :
    chartAt (ModelProd HB (F₁ →L[𝕜] F₂)) y₀ y =
      (chartAt HB y₀.1 y.1, inCoordinates F₁ E₁ F₂ E₂ y₀.1 y.1 y₀.1 y.1 y.2)

Proof state:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E₁ x)
inst✝¹⁸ : NormedAddCommGroup F₁
inst✝¹⁷ : NormedSpace 𝕜 F₁
inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝¹⁴ : (x : B) → AddCommGroup (E₂ x)
inst✝¹³ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → TopologicalSpace (E₂ x)
HB : Type u_9
inst✝⁸ : TopologicalSpace HB
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
inst✝⁵ : FiberBundle F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₁ E₁
inst✝³ : FiberBundle F₂ E₂
inst✝² : VectorBundle 𝕜 F₂ E₂
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
y₀ y : LE₁E₂
⊢ ↑(chartAt (ModelProd HB (F₁ →L[𝕜] F₂)) y₀) y =
    (↑(chartAt HB y₀.proj) y.proj, inCoordinates F₁ E₁ F₂ E₂ y₀.proj y.proj y₀.proj y.proj y.snd)

Tactic:
rw [FiberBundle.chartedSpace_chartAt, trans_apply, PartialHomeomorph.prod_apply,
  Trivialization.coe_coe, PartialHomeomorph.refl_apply, Function.id_def,
  hom_trivializationAt_apply]

Result:
no goals
-- Mathlib/Data/Quot.lean
theorem Quotient.mk_eq_iff_out {s : Setoid α} {x : α} {y : Quotient s} :
    ⟦x⟧ = y ↔ x ≈ Quotient.out y

Proof state:
α : Sort u_1
s : Setoid α
x : α
y : Quotient s
⊢ ⟦x⟧ = y ↔ x ≈ y.out

Tactic:
refine Iff.trans ?_ Quotient.eq

Result:
α : Sort u_1
s : Setoid α
x : α
y : Quotient s
⊢ ⟦x⟧ = y ↔ ⟦x⟧ = ⟦y.out⟧

Proof state:
α : Sort u_1
s : Setoid α
x : α
y : Quotient s
⊢ ⟦x⟧ = y ↔ ⟦x⟧ = ⟦y.out⟧

Tactic:
rw [Quotient.out_eq y]

Result:
no goals