harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Pell.lean
theorem x_mul_y_le_y_mul_x {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d}
    (hax : 1 < a.x) (hay : 0 < a.y) : a.x * a₁.y ≤ a.y * a₁.x

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.x * a₁.y ≤ a.y * a₁.x

Tactic:
rw [← abs_of_pos <| zero_lt_one.trans hax, ← abs_of_pos hay, ← abs_of_pos h.x_pos, ←
  abs_of_pos h.2.1, ← abs_mul, ← abs_mul, ← sq_le_sq, mul_pow, mul_pow, a.prop_x, a₁.prop_x, ←
  sub_nonneg]

Result:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 ≤ a.y ^ 2 * (1 + d * a₁.y ^ 2) - (1 + d * a.y ^ 2) * a₁.y ^ 2

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a₁.y ≤ a.y

Tactic:
exact h.y_le_y hax hay

Result:
no goals

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 ≤ a.y ^ 2 - a₁.y ^ 2

Tactic:
rw [sub_nonneg, sq_le_sq, abs_of_pos hay, abs_of_pos h.2.1]

Result:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a₁.y ≤ a.y

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 ≤ a.y ^ 2 * (1 + d * a₁.y ^ 2) - (1 + d * a.y ^ 2) * a₁.y ^ 2

Tactic:
ring_nf

Result:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 ≤ a.y ^ 2 - a₁.y ^ 2
-- Mathlib/Data/Fintype/Inv.lean
theorem choose_subtype_eq {α : Type*} (p : α → Prop) [Fintype { a : α // p a }] [DecidableEq α]
    (x : { a : α // p a })
    (h : ∃! a : { a // p a }, (a : α) = x :=
      ⟨x, rfl, fun y hy => by simpa [Subtype.ext_iff] using hy⟩) :
    Fintype.choose (fun y : { a : α // p a } => (y : α) = x) h = x

Proof state:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α✝
p✝ : α✝ → Prop
inst✝² : DecidablePred p✝
α : Type u_4
p : α → Prop
inst✝¹ : Fintype { a // p a }
inst✝ : DecidableEq α
x y : { a // p a }
hy : (fun a => ↑a = ↑x) y
⊢ y = x

Tactic:
simpa [Subtype.ext_iff] using hy

Result:
no goals

Proof state:
α : Type u_4
p : α → Prop
inst✝¹ : Fintype { a // p a }
inst✝ : DecidableEq α
x : { a // p a }
h : optParam (∃! a, ↑a = ↑x) ⋯
⊢ choose (fun y => ↑y = ↑x) h = x

Tactic:
rw [Subtype.ext_iff, Fintype.choose_spec (fun y : { a : α // p a } => (y : α) = x) _]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem diam_range (hf : Isometry f) : Metric.diam (range f) = Metric.diam (univ : Set α)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.diam (f '' univ) = Metric.diam univ

Tactic:
exact hf.diam_image univ

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.diam (range f) = Metric.diam univ

Tactic:
rw [← image_univ]

Result:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.diam (f '' univ) = Metric.diam univ
-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean
@[simp] lemma ENNReal.exp_log (x : ℝ≥0∞) : exp (log x) = x

Proof state:
case neg
x : ℝ≥0∞
hx_top : ¬x = ⊤
hx_zero : ¬x = 0
⊢ x.log.exp = x

Tactic:
have hx_pos : 0 < x.toReal := ENNReal.toReal_pos hx_zero hx_top

Result:
case neg
x : ℝ≥0∞
hx_top : ¬x = ⊤
hx_zero : ¬x = 0
hx_pos : 0 < x.toReal
⊢ x.log.exp = x

Proof state:
case pos
x : ℝ≥0∞
hx_top : x = ⊤
⊢ x.log.exp = x

Tactic:
simp [hx_top]

Result:
no goals

Proof state:
case pos
x : ℝ≥0∞
hx_top : ¬x = ⊤
hx_zero : x = 0
⊢ x.log.exp = x

Tactic:
simp [hx_zero]

Result:
no goals

Proof state:
case neg
x : ℝ≥0∞
hx_top : ¬x = ⊤
⊢ x.log.exp = x

Tactic:
by_cases hx_zero : x = 0

Result:
case pos
x : ℝ≥0∞
hx_top : ¬x = ⊤
hx_zero : x = 0
⊢ x.log.exp = x

case neg
x : ℝ≥0∞
hx_top : ¬x = ⊤
hx_zero : ¬x = 0
⊢ x.log.exp = x

Proof state:
x : ℝ≥0∞
⊢ x.log.exp = x

Tactic:
by_cases hx_top : x = ∞

Result:
case pos
x : ℝ≥0∞
hx_top : x = ⊤
⊢ x.log.exp = x

case neg
x : ℝ≥0∞
hx_top : ¬x = ⊤
⊢ x.log.exp = x

Proof state:
case neg
x : ℝ≥0∞
hx_top : ¬x = ⊤
hx_zero : ¬x = 0
hx_pos : 0 < x.toReal
⊢ x.log.exp = x

Tactic:
rw [← ENNReal.ofReal_toReal hx_top, log_ofReal_of_pos hx_pos, exp_coe, Real.exp_log hx_pos]

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
lemma continuous_iff {Y : Type*} [TopologicalSpace Y] (f : OnePoint X → Y) : Continuous f ↔
    Tendsto (fun x : X ↦ f x) (coclosedCompact X) (𝓝 (f ∞)) ∧ Continuous (fun x : X ↦ f x)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
⊢ Continuous f ↔ Tendsto (fun x => f ↑x) (coclosedCompact X) (𝓝 (f ∞)) ∧ Continuous fun x => f ↑x

Tactic:
simp only [continuous_iff_continuousAt, OnePoint.forall, continuousAt_coe, continuousAt_infty',
  Function.comp_def]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma equation_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W'.Equation P ↔ W'.Equation Q

Proof state:
case intro
R : Type r
inst✝ : CommRing R
W' : Jacobian R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Equation ((fun m => m • Q) u) ↔ W'.Equation Q

Tactic:
exact equation_smul Q u.isUnit

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.Equation P ↔ W'.Equation Q

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
W' : Jacobian R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Equation ((fun m => m • Q) u) ↔ W'.Equation Q
-- Mathlib/FieldTheory/JacobsonNoether.lean
/-- If `D` is a purely inseparable extension of `k` with characteristic `p`,
  then for every element `a` of `D \ k`, there exists a natural number `n`
  **greater than 0** such that `a ^ (p ^ n)` is contained in `k`. -/
lemma exists_pow_mem_center_of_inseparable' (p : ℕ) [ExpChar D p] {a : D}
    (ha : a ∉ k) (hinsep : ∀ x : D, IsSeparable k x → x ∈ k) : ∃ n, 1 ≤ n ∧ a ^ (p ^ n) ∈ k

Proof state:
case pos
D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
n : ℕ
hn : a ∈ k
nzero : n = 0
⊢ ∃ n, 1 ≤ n ∧ a ^ p ^ n ∈ k

Tactic:
exact (ha hn).elim

Result:
no goals

Proof state:
case neg
D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
n : ℕ
hn : a ^ p ^ n ∈ k
nzero : ¬n = 0
⊢ ∃ n, 1 ≤ n ∧ a ^ p ^ n ∈ k

Tactic:
exact ⟨n, ⟨Nat.one_le_iff_ne_zero.mpr nzero, hn⟩⟩

Result:
no goals

Proof state:
D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
⊢ ∃ n, 1 ≤ n ∧ a ^ p ^ n ∈ k

Tactic:
obtain ⟨n, hn⟩ := exists_pow_mem_center_of_inseparable p a hinsep

Result:
case intro
D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
n : ℕ
hn : a ^ p ^ n ∈ k
⊢ ∃ n, 1 ≤ n ∧ a ^ p ^ n ∈ k

Proof state:
case intro
D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
n : ℕ
hn : a ^ p ^ n ∈ k
⊢ ∃ n, 1 ≤ n ∧ a ^ p ^ n ∈ k

Tactic:
by_cases nzero : n = 0

Result:
case pos
D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
n : ℕ
hn : a ^ p ^ n ∈ k
nzero : n = 0
⊢ ∃ n, 1 ≤ n ∧ a ^ p ^ n ∈ k

case neg
D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
n : ℕ
hn : a ^ p ^ n ∈ k
nzero : ¬n = 0
⊢ ∃ n, 1 ≤ n ∧ a ^ p ^ n ∈ k

Proof state:
case pos
D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
n : ℕ
hn : a ^ p ^ n ∈ k
nzero : n = 0
⊢ ∃ n, 1 ≤ n ∧ a ^ p ^ n ∈ k

Tactic:
rw [nzero, pow_zero, pow_one] at hn

Result:
case pos
D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
n : ℕ
hn : a ∈ k
nzero : n = 0
⊢ ∃ n, 1 ≤ n ∧ a ^ p ^ n ∈ k
-- Mathlib/Data/Finset/Density.lean
@[simp] lemma dens_cons (h : a ∉ s) : (s.cons a h).dens = dens s + (Fintype.card α : ℚ≥0)⁻¹

Proof state:
α : Type u_2
inst✝ : Fintype α
s : Finset α
a : α
h : a ∉ s
⊢ (cons a s h).dens = s.dens + (↑(Fintype.card α))⁻¹

Tactic:
simp [dens, add_div]

Result:
no goals
-- Mathlib/LinearAlgebra/Orientation.lean
theorem orientation_adjustToOrientation [Nonempty ι] (e : Basis ι R M)
    (x : Orientation R M ι) : (e.adjustToOrientation x).orientation = x

Proof state:
case pos
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : e.orientation = x
⊢ e.orientation = x

Tactic:
exact h

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
⊢ (if e.orientation = x then e else e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))).orientation = x

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : e.orientation = x
⊢ e.orientation = x

case neg
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : ¬e.orientation = x
⊢ (e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))).orientation = x

Proof state:
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
⊢ (e.adjustToOrientation x).orientation = x

Tactic:
rw [adjustToOrientation]

Result:
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
⊢ (if e.orientation = x then e else e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))).orientation = x

Proof state:
case neg
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : ¬e.orientation = x
⊢ (e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))).orientation = x

Tactic:
rw [orientation_neg_single, eq_comm, ← orientation_ne_iff_eq_neg, ne_comm]

Result:
case neg
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : ¬e.orientation = x
⊢ e.orientation ≠ x

Proof state:
case neg
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : ¬e.orientation = x
⊢ e.orientation ≠ x

Tactic:
exact h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem unattach_filter {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → Bool} {g : α → Bool} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
    (l.filter f).unattach = l.unattach.filter g

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ (filter f l).unattach = filter g l.unattach

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  simp only [filter_cons, hf, unattach_cons]
  split <;> simp [ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ (filter f []).unattach = filter g [].unattach

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : (filter f l).unattach = filter g l.unattach
⊢ (filter f (a :: l)).unattach = filter g (a :: l).unattach

Tactic:
simp only [filter_cons, hf, unattach_cons]

Result:
case cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : (filter f l).unattach = filter g l.unattach
⊢ (if g a.val = true then a :: filter f l else filter f l).unattach =
    if g a.val = true then a.val :: filter g l.unattach else filter g l.unattach

Proof state:
case cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : (filter f l).unattach = filter g l.unattach
⊢ (if g a.val = true then a :: filter f l else filter f l).unattach =
    if g a.val = true then a.val :: filter g l.unattach else filter g l.unattach

Tactic:
split <;> simp [ih]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.ro_eq_true_of_ro (u v k₁ k₂ : Nat) : isLE k₁ k₂ = true → u ≤ v + k₁ → (u ≤ v + k₂) = True :=
  by simp [isLE]; omega

Proof state:
u v k₁ k₂ : Nat
⊢ k₁ ≤ k₂ → u ≤ v + k₁ → u ≤ v + k₂

Tactic:
omega

Result:
no goals

Proof state:
u v k₁ k₂ : Nat
⊢ isLE k₁ k₂ = true → u ≤ v + k₁ → (u ≤ v + k₂) = True

Tactic:
simp [isLE]

Result:
u v k₁ k₂ : Nat
⊢ k₁ ≤ k₂ → u ≤ v + k₁ → u ≤ v + k₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem unzip_zip {l₁ : Vector α n} {l₂ : Vector β n} :
    unzip (zip l₁ l₂) = (l₁, l₂)

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h }).unzip =
    ({ toArray := l₁, size_toArray := ⋯ }, { toArray := l₂, size_toArray := h })

Tactic:
simp [Array.unzip_zip, h, Array.map_fst_zip, Array.map_snd_zip]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l₁ : Vector α n
l₂ : Vector β n
⊢ (l₁.zip l₂).unzip = (l₁, l₂)

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Vector β l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip l₂).unzip = ({ toArray := l₁, size_toArray := ⋯ }, l₂)

Proof state:
case mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Vector β l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip l₂).unzip = ({ toArray := l₁, size_toArray := ⋯ }, l₂)

Tactic:
rcases l₂ with ⟨l₂, h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h }).unzip =
    ({ toArray := l₁, size_toArray := ⋯ }, { toArray := l₂, size_toArray := h })
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attachWith_push {a : α} {l : Array α} {P : α → Prop} {H : ∀ x ∈ l.push a, P x} :
    (l.push a).attachWith P H =
      (l.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩

Proof state:
case mk
α : Type u_1
a : α
P : α → Prop
toList✝ : List α
H : ∀ (x : α), x ∈ { toList := toList✝ }.push a → P x
⊢ ({ toList := toList✝ }.push a).attachWith P H = ({ toList := toList✝ }.attachWith P ⋯).push ⟨a, ⋯⟩

Tactic:
simp [attachWith_congr (List.push_toArray _ _)]

Result:
no goals

Proof state:
α : Type ?u.16231
a : α
l : Array α
P : α → Prop
x : α
h : x ∈ l
H : ∀ (x : α), x ∈ l ∨ x = a → P x
⊢ P x

Tactic:
exact H x (.inl h)

Result:
no goals

Proof state:
α : Type u_1
a : α
l : Array α
P : α → Prop
H : ∀ (x : α), x ∈ l.push a → P x
⊢ (l.push a).attachWith P H = (l.attachWith P ⋯).push ⟨a, ⋯⟩

Tactic:
cases l

Result:
case mk
α : Type u_1
a : α
P : α → Prop
toList✝ : List α
H : ∀ (x : α), x ∈ { toList := toList✝ }.push a → P x
⊢ ({ toList := toList✝ }.push a).attachWith P H = ({ toList := toList✝ }.attachWith P ⋯).push ⟨a, ⋯⟩

Proof state:
α : Type ?u.16231
a : α
l : Array α
P : α → Prop
H : ∀ (x : α), x ∈ l.push a → P x
x : α
h : x ∈ l
⊢ P x

Tactic:
simp at H

Result:
α : Type ?u.16231
a : α
l : Array α
P : α → Prop
x : α
h : x ∈ l
H : ∀ (x : α), x ∈ l ∨ x = a → P x
⊢ P x

Proof state:
α : Type ?u.16231
a : α
l : Array α
P : α → Prop
H : ∀ (x : α), x ∈ l.push a → P x
⊢ a ∈ l.push a

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem inv_congr {R} [DivisionRing R] {a a' b : R} (_ : a = a')
    (_ : a'⁻¹ = b) : (a⁻¹ : R) = b

Proof state:
R : Type u_2
inst✝ : DivisionRing R
a' : R
⊢ a'⁻¹ = a'⁻¹

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_2
inst✝ : DivisionRing R
a a' b : R
x✝¹ : a = a'
x✝ : a'⁻¹ = b
⊢ a⁻¹ = b

Tactic:
subst_vars

Result:
R : Type u_2
inst✝ : DivisionRing R
a' : R
⊢ a'⁻¹ = a'⁻¹
-- Mathlib/Data/Finset/Image.lean
theorem finsetCongr_refl : (Equiv.refl α).finsetCongr = Equiv.refl _

Proof state:
α : Type u_1
⊢ (Equiv.refl α).finsetCongr = Equiv.refl (Finset α)

Tactic:
ext

Result:
case H.h
α : Type u_1
x✝ : Finset α
a✝ : α
⊢ a✝ ∈ (Equiv.refl α).finsetCongr x✝ ↔ a✝ ∈ (Equiv.refl (Finset α)) x✝

Proof state:
case H.h
α : Type u_1
x✝ : Finset α
a✝ : α
⊢ a✝ ∈ (Equiv.refl α).finsetCongr x✝ ↔ a✝ ∈ (Equiv.refl (Finset α)) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem map_mono {f : α → β} (h : μ ≤ ν) (hf : Measurable f) : μ.map f ≤ ν.map f :=
  le_iff.2 fun s hs ↦ by simp [hf.aemeasurable, hs, h _]

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
f : α → β
h : μ ≤ ν
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (map f μ) s ≤ (map f ν) s

Tactic:
simp [hf.aemeasurable, hs, h _]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_measure_zero (hT : DominatedFinMeasAdditive μ T C) (h : μ = 0) :
    setToFun μ T hT f = 0

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h : μ = 0
⊢ setToFun μ T hT f = 0

Tactic:
have : f =ᵐ[μ] 0 := by simp [h, EventuallyEq]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h : μ = 0
this : f =ᶠ[ae μ] 0
⊢ setToFun μ T hT f = 0

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h : μ = 0
this : f =ᶠ[ae μ] 0
⊢ setToFun μ T hT f = 0

Tactic:
rw [setToFun_congr_ae hT this, setToFun_zero]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h : μ = 0
⊢ f =ᶠ[ae μ] 0

Tactic:
simp [h, EventuallyEq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
theorem log_surjective : Function.Surjective log

Proof state:
case h
y : EReal
y_nbot : ⊥ < y
y_ntop : y < ⊤
exp_y_pos : ¬Real.exp y.toReal ≤ 0
⊢ (ENNReal.ofReal (Real.exp y.toReal)).log = y

Tactic:
simp only [log, ofReal_eq_zero, exp_y_pos, ↓reduceIte, ofReal_ne_top,
  ENNReal.toReal_ofReal (Real.exp_pos y.toReal).le, Real.log_exp y.toReal]

Result:
case h
y : EReal
y_nbot : ⊥ < y
y_ntop : y < ⊤
exp_y_pos : ¬Real.exp y.toReal ≤ 0
⊢ ↑y.toReal = y

Proof state:
⊢ Function.Surjective log

Tactic:
intro y

Result:
y : EReal
⊢ ∃ a, a.log = y

Proof state:
case inr.inl
y : EReal
y_nbot : ⊥ < y
y_top : y = ⊤
⊢ ∃ a, a.log = y

Tactic:
exact y_top ▸ ⟨⊤, log_top⟩

Result:
no goals

Proof state:
y : EReal
⊢ ∃ a, a.log = y

Tactic:
rcases eq_bot_or_bot_lt y with y_bot | y_nbot

Result:
case inl
y : EReal
y_bot : y = ⊥
⊢ ∃ a, a.log = y

case inr
y : EReal
y_nbot : ⊥ < y
⊢ ∃ a, a.log = y

Proof state:
case inr.inr
y : EReal
y_nbot : ⊥ < y
y_ntop : y < ⊤
⊢ ∃ a, a.log = y

Tactic:
use ENNReal.ofReal (Real.exp y.toReal)

Result:
case h
y : EReal
y_nbot : ⊥ < y
y_ntop : y < ⊤
⊢ (ENNReal.ofReal (Real.exp y.toReal)).log = y

Proof state:
case inr
y : EReal
y_nbot : ⊥ < y
⊢ ∃ a, a.log = y

Tactic:
rcases eq_top_or_lt_top y with y_top | y_ntop

Result:
case inr.inl
y : EReal
y_nbot : ⊥ < y
y_top : y = ⊤
⊢ ∃ a, a.log = y

case inr.inr
y : EReal
y_nbot : ⊥ < y
y_ntop : y < ⊤
⊢ ∃ a, a.log = y

Proof state:
case inl
y : EReal
y_bot : y = ⊥
⊢ ∃ a, a.log = y

Tactic:
exact y_bot ▸ ⟨⊥, log_zero⟩

Result:
no goals

Proof state:
case h
y : EReal
y_nbot : ⊥ < y
y_ntop : y < ⊤
⊢ (ENNReal.ofReal (Real.exp y.toReal)).log = y

Tactic:
have exp_y_pos := not_le_of_lt (Real.exp_pos y.toReal)

Result:
case h
y : EReal
y_nbot : ⊥ < y
y_ntop : y < ⊤
exp_y_pos : ¬Real.exp y.toReal ≤ 0
⊢ (ENNReal.ofReal (Real.exp y.toReal)).log = y

Proof state:
case h
y : EReal
y_nbot : ⊥ < y
y_ntop : y < ⊤
exp_y_pos : ¬Real.exp y.toReal ≤ 0
⊢ ↑y.toReal = y

Tactic:
exact EReal.coe_toReal y_ntop.ne y_nbot.ne'

Result:
no goals