harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem coe_of_h_rat_eq (v_eq_q : v = (↑q : K)) : (↑((of q).h : ℚ) : K) = (of v).h

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ ↑(of q).h = (of v).h

Tactic:
unfold of IntFractPair.seq1

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ ↑(match (IntFractPair.of q, Stream'.Seq.tail ⟨IntFractPair.stream q, ⋯⟩) with
        | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h =
    (match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
      | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ ↑(match (IntFractPair.of q, Stream'.Seq.tail ⟨IntFractPair.stream q, ⋯⟩) with
        | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h =
    (match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
      | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h

Tactic:
rw [← IntFractPair.coe_of_rat_eq v_eq_q]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ ↑(match (IntFractPair.of q, Stream'.Seq.tail ⟨IntFractPair.stream q, ⋯⟩) with
        | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h =
    (match (IntFractPair.mapFr Rat.cast (IntFractPair.of q), Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
      | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ ↑(match (IntFractPair.of q, Stream'.Seq.tail ⟨IntFractPair.stream q, ⋯⟩) with
        | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h =
    (match (IntFractPair.mapFr Rat.cast (IntFractPair.of q), Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
      | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem modEq_neg : a ≡ b [PMOD -p] ↔ a ≡ b [PMOD p] :=
  modEq_comm.trans <| by simp [ModEq, ← neg_eq_iff_eq_neg]

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b : α
⊢ b ≡ a [PMOD -p] ↔ a ≡ b [PMOD p]

Tactic:
simp [ModEq, ← neg_eq_iff_eq_neg]

Result:
no goals
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem coeff_zero_mem_comap_of_root_mem_of_eval_mem {r : S} (hr : r ∈ I) {p : R[X]}
    (hp : p.eval₂ f r ∈ I) : p.coeff 0 ∈ I.comap f

Proof state:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r p.divX * r + f (p.coeff 0) ∈ I
⊢ p.coeff 0 ∈ comap f I

Tactic:
refine mem_comap.mpr ((I.add_mem_iff_right ?_).mp hp)

Result:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r p.divX * r + f (p.coeff 0) ∈ I
⊢ eval₂ f r p.divX * r ∈ I

Proof state:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r p.divX * r + f (p.coeff 0) ∈ I
⊢ eval₂ f r p.divX * r ∈ I

Tactic:
exact I.mul_mem_left _ hr

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r p ∈ I
⊢ p.coeff 0 ∈ comap f I

Tactic:
rw [← p.divX_mul_X_add, eval₂_add, eval₂_C, eval₂_mul, eval₂_X] at hp

Result:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r p.divX * r + f (p.coeff 0) ∈ I
⊢ p.coeff 0 ∈ comap f I
-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem w_mul_φ_nonneg (D : ℝ) (x y : E) : 0 ≤ w D y * φ (x - y) :=
  mul_nonneg (w_nonneg D y) (indicator_nonneg (by simp only [zero_le_one, imp_true_iff]) _)

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x y : E
⊢ ∀ a ∈ closedBall 0 1, 0 ≤ 1

Tactic:
simp only [zero_le_one, imp_true_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean
theorem descFOne_zero_comm {Y Z : C} (f : Z ⟶ Y) (I : InjectiveResolution Y)
    (J : InjectiveResolution Z) :
    J.cocomplex.d 0 1 ≫ descFOne f I J = descFZero f I J ≫ I.cocomplex.d 0 1

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ J.cocomplex.d 0 1 ≫ descFOne f I J = descFZero f I J ≫ I.cocomplex.d 0 1

Tactic:
apply J.exact₀.comp_descToInjective

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
@[simp] lemma in₂₁_iff : (graph t).Adj (in₂ c) (in₁ b) ↔ ∃ a, (a, b, c) ∈ t :=
  ⟨by rintro ⟨⟩; exact ⟨_, ‹_›⟩, fun ⟨_, h⟩ ↦ in₂₁ h⟩

Proof state:
case in₂₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ a, (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
⊢ (graph t).Adj (in₂ c) (in₁ b) → ∃ a, (a, b, c) ∈ t

Tactic:
rintro ⟨⟩

Result:
case in₂₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ a, (a, b, c) ∈ t
-- Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
theorem aux₀ {v : ℤ} (hv : 0 < v) : (0 : ℝ) < v ∧ (0 : ℝ) < 2 * v - 1 :=
  ⟨cast_pos.mpr hv, by norm_cast; omega⟩

Proof state:
v : ℤ
hv : 0 < v
⊢ 0 < 2 * v - 1

Tactic:
omega

Result:
no goals

Proof state:
v : ℤ
hv : 0 < v
⊢ 0 < 2 * ↑v - 1

Tactic:
norm_cast

Result:
v : ℤ
hv : 0 < v
⊢ 0 < 2 * v - 1
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
lemma preNormEDS'_odd (m : ℕ) : preNormEDS' b c d (2 * (m + 2) + 1) =
    preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * (if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * (if Even m then 1 else b)

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ ((preNormEDS' b c d (2 * m / 2 + 4) * preNormEDS' b c d (2 * m / 2 + 2) ^ 3 * if Even (2 * m / 2) then b else 1) -
      preNormEDS' b c d (2 * m / 2 + 1) * preNormEDS' b c d (2 * m / 2 + 3) ^ 3 * if Even (2 * m / 2) then 1 else b) =
    (preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * if Even m then 1 else b

Tactic:
simp only [m.mul_div_cancel_left two_pos]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ 2 * (m + 2) + 1 = 2 * m + 5

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS' b c d (2 * (m + 2) + 1) =
    (preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * if Even m then 1 else b

Tactic:
rw [show 2 * (m + 2) + 1 = 2 * m + 5 by rfl, preNormEDS', dif_pos <| even_two_mul _]

Result:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ ((preNormEDS' b c d (2 * m / 2 + 4) * preNormEDS' b c d (2 * m / 2 + 2) ^ 3 * if Even (2 * m / 2) then b else 1) -
      preNormEDS' b c d (2 * m / 2 + 1) * preNormEDS' b c d (2 * m / 2 + 3) ^ 3 * if Even (2 * m / 2) then 1 else b) =
    (preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * if Even m then 1 else b
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
lemma injOn_pow_mul {n : ℕ} {ζ : M₀} (hζ : IsPrimitiveRoot ζ n) {α : M₀} (hα : α ≠ 0) :
    Set.InjOn (ζ ^ · * α) (Finset.range n) :=
  fun i hi j hj e ↦
    hζ.injOn_pow hi hj (by simpa [mul_eq_mul_right_iff, or_iff_left hα] using e)

Proof state:
M₀ : Type u_7
inst✝ : CancelCommMonoidWithZero M₀
n : ℕ
ζ : M₀
hζ : IsPrimitiveRoot ζ n
α : M₀
hα : α ≠ 0
i : ℕ
hi : i ∈ ↑(range n)
j : ℕ
hj : j ∈ ↑(range n)
e : (fun x => ζ ^ x * α) i = (fun x => ζ ^ x * α) j
⊢ (fun x => ζ ^ x) i = (fun x => ζ ^ x) j

Tactic:
simpa [mul_eq_mul_right_iff, or_iff_left hα] using e

Result:
no goals
-- Mathlib/Algebra/Order/Disjointed.lean
protected lemma Monotone.disjointed_add_one [NoMaxOrder ι]  {f : ι → α} (hf : Monotone f) (i : ι) :
    disjointed f (i + 1) = f (i + 1) \ f i

Proof state:
α : Type u_1
ι : Type u_2
inst✝⁶ : GeneralizedBooleanAlgebra α
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : Add ι
inst✝² : One ι
inst✝¹ : SuccAddOrder ι
inst✝ : NoMaxOrder ι
f : ι → α
hf : Monotone f
i : ι
⊢ ¬IsMax i

Tactic:
exact not_isMax i

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝⁶ : GeneralizedBooleanAlgebra α
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : Add ι
inst✝² : One ι
inst✝¹ : SuccAddOrder ι
inst✝ : NoMaxOrder ι
f : ι → α
hf : Monotone f
i : ι
⊢ disjointed f (i + 1) = f (i + 1) \ f i

Tactic:
rw [← succ_eq_add_one, hf.disjointed_succ]

Result:
α : Type u_1
ι : Type u_2
inst✝⁶ : GeneralizedBooleanAlgebra α
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : Add ι
inst✝² : One ι
inst✝¹ : SuccAddOrder ι
inst✝ : NoMaxOrder ι
f : ι → α
hf : Monotone f
i : ι
⊢ ¬IsMax i
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem gcd (hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x) :
    IsPeriodicPt f (m.gcd n) x

Proof state:
case refine_2
α : Type u_1
f : α → α
x : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f ((n % m).gcd m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f ((n % m).gcd m) x

Tactic:
exact ih (hn.mod hm) hm

Result:
no goals

Proof state:
case refine_2
α : Type u_1
f : α → α
x : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f ((n % m).gcd m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m.gcd n) x

Tactic:
rw [Nat.gcd_rec]

Result:
case refine_2
α : Type u_1
f : α → α
x : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f ((n % m).gcd m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f ((n % m).gcd m) x

Proof state:
case refine_1
α : Type u_1
f : α → α
x : α
m n✝ n : ℕ
x✝ : IsPeriodicPt f 0 x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd 0 n) x

Tactic:
rwa [Nat.gcd_zero_left]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m.gcd n) x

Tactic:
revert hm hn

Result:
α : Type u_1
f : α → α
x : α
m n : ℕ
⊢ IsPeriodicPt f m x → IsPeriodicPt f n x → IsPeriodicPt f (m.gcd n) x

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
⊢ IsPeriodicPt f m x → IsPeriodicPt f n x → IsPeriodicPt f (m.gcd n) x

Tactic:
refine Nat.gcd.induction m n (fun n _ hn => ?_) fun m n _ ih hm hn => ?_

Result:
case refine_1
α : Type u_1
f : α → α
x : α
m n✝ n : ℕ
x✝ : IsPeriodicPt f 0 x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd 0 n) x

case refine_2
α : Type u_1
f : α → α
x : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f ((n % m).gcd m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m.gcd n) x
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem norm_eq_one_iff' {d : ℤ} (hd : d ≤ 0) (z : ℤ√d) : z.norm = 1 ↔ IsUnit z

Proof state:
d : ℤ
hd : d ≤ 0
z : ℤ√d
⊢ z.norm = 1 ↔ IsUnit z

Tactic:
rw [← norm_eq_one_iff, ← Int.natCast_inj, Int.natAbs_of_nonneg (norm_nonneg hd z), Int.ofNat_one]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_eq_left : a ∆ b = a ↔ b = ⊥ :=
  calc
    a ∆ b = a ↔ a ∆ b = a ∆ ⊥

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

Tactic:
rw [symmDiff_right_inj]

Result:
no goals

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

Tactic:
rw [symmDiff_bot]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem of_map_inf [SemilatticeInf α] [SemilatticeSup β]
    (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊔ f y) : AntitoneOn f s := fun x hx y hy hxy =>
  sup_eq_left.1 <| by rw [← h _ hx _ hy, inf_eq_left.2 hxy]

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeSup β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊓ y) = f x ⊔ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ f x ⊔ f y = f x

Tactic:
rw [← h _ hx _ hy, inf_eq_left.2 hxy]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
@[simp]
lemma restrict_compl_nullSet (h : μ ⟂ₘ ν) : ν.restrict h.nullSetᶜ = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ ν.restrict h.nullSetᶜ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem reflTransGen_iff_eq_or_transGen : ReflTransGen r a b ↔ b = a ∨ TransGen r a b

Proof state:
case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : b = a ∨ TransGen r a b
⊢ ReflTransGen r a b

Tactic:
rcases h with (rfl | h)

Result:
case refine_2.inl
α : Type u_1
r : α → α → Prop
b : α
⊢ ReflTransGen r b b

case refine_2.inr
α : Type u_1
r : α → α → Prop
a b : α
h : TransGen r a b
⊢ ReflTransGen r a b

Proof state:
case refine_2.inr
α : Type u_1
r : α → α → Prop
a b : α
h : TransGen r a b
⊢ ReflTransGen r a b

Tactic:
exact h.to_reflTransGen

Result:
no goals

Proof state:
case refine_1.refl
α : Type u_1
r : α → α → Prop
a : α
⊢ a = a ∨ TransGen r a a

Tactic:
exact Or.inl rfl

Result:
no goals

Proof state:
case refine_1
α : Type u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
⊢ b = a ∨ TransGen r a b

Tactic:
cases h with
| refl => exact Or.inl rfl
| tail hac hcb => exact Or.inr (TransGen.tail' hac hcb)

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen r a b ↔ b = a ∨ TransGen r a b

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
α : Type u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
⊢ b = a ∨ TransGen r a b

case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : b = a ∨ TransGen r a b
⊢ ReflTransGen r a b

Proof state:
case refine_1.tail
α : Type u_1
r : α → α → Prop
a b b✝ : α
hac : ReflTransGen r a b✝
hcb : r b✝ b
⊢ b = a ∨ TransGen r a b

Tactic:
exact Or.inr (TransGen.tail' hac hcb)

Result:
no goals

Proof state:
case refine_2.inl
α : Type u_1
r : α → α → Prop
b : α
⊢ ReflTransGen r b b

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Filter/CountableSeparatingOn.lean
theorem exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating (p : Set α → Prop)
    {s : Set α} [HasCountableSeparatingOn α p s] (hs : s ∈ l) (hne : s.Nonempty)
    (hl : ∀ U, p U → U ∈ l ∨ Uᶜ ∈ l) : ∃ a ∈ s, {a} ∈ l

Proof state:
case intro.intro.intro.inr.intro
α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
x : α
hts : {x} ⊆ s
ht : {x}.Subsingleton
htl : {x} ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
exact ⟨x, hts rfl, htl⟩

Result:
no goals

Proof state:
α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
rcases exists_subset_subsingleton_mem_of_forall_separating p hs hl with ⟨t, hts, ht, htl⟩

Result:
case intro.intro.intro
α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
t : Set α
hts : t ⊆ s
ht : t.Subsingleton
htl : t ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Proof state:
case intro.intro.intro
α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
t : Set α
hts : t ⊆ s
ht : t.Subsingleton
htl : t ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
rcases ht.eq_empty_or_singleton with rfl | ⟨x, rfl⟩

Result:
case intro.intro.intro.inl
α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hts : ∅ ⊆ s
ht : ∅.Subsingleton
htl : ∅ ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

case intro.intro.intro.inr.intro
α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
x : α
hts : {x} ⊆ s
ht : {x}.Subsingleton
htl : {x} ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Proof state:
case intro.intro.intro.inl
α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hts : ∅ ⊆ s
ht : ∅.Subsingleton
htl : ∅ ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
exact hne.imp fun a ha ↦ ⟨ha, mem_of_superset htl (empty_subset _)⟩

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_add_left {m : MeasurableSpace α} (T T' : Set α → F →L[ℝ] F') {f : α →ₛ F} :
    setToSimpleFunc (T + T') f = setToSimpleFunc T f + setToSimpleFunc T' f

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})) x =
    ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x + ∑ x ∈ f.range, (T' (⇑f ⁻¹' {x})) x

Tactic:
push_cast

Result:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x ∈ f.range, (⇑(T (⇑f ⁻¹' {x})) + ⇑(T' (⇑f ⁻¹' {x}))) x =
    ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x + ∑ x ∈ f.range, (T' (⇑f ⁻¹' {x})) x

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x ∈ f.range, (⇑(T (⇑f ⁻¹' {x})) + ⇑(T' (⇑f ⁻¹' {x}))) x =
    ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x + ∑ x ∈ f.range, (T' (⇑f ⁻¹' {x})) x

Tactic:
simp_rw [Pi.add_apply, sum_add_distrib]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ setToSimpleFunc (T + T') f = setToSimpleFunc T f + setToSimpleFunc T' f

Tactic:
simp_rw [setToSimpleFunc, Pi.add_apply]

Result:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})) x =
    ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x + ∑ x ∈ f.range, (T' (⇑f ⁻¹' {x})) x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem expand.go_neg [Hashable α] {i : Nat} {source : Array (AssocList α β)}
    {target : { d : Array (AssocList α β) // 0 < d.size}} (h : ¬i < source.size) :
    expand.go i source target = target

Proof state:
α : Type u
β : α → Type v
inst✝ : Hashable α
i : Nat
source : Array (AssocList α β)
target : { d // 0 < d.size }
h : ¬i < source.size
⊢ (if h : i < source.size then
      let es := source[i];
      let source := source.set i AssocList.nil h;
      let target := AssocList.foldl (reinsertAux hash) target es;
      go (i + 1) source target
    else target) =
    target

Tactic:
simp only [h, dite_false]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : Hashable α
i : Nat
source : Array (AssocList α β)
target : { d // 0 < d.size }
h : ¬i < source.size
⊢ go i source target = target

Tactic:
rw [expand.go]

Result:
α : Type u
β : α → Type v
inst✝ : Hashable α
i : Nat
source : Array (AssocList α β)
target : { d // 0 < d.size }
h : ¬i < source.size
⊢ (if h : i < source.size then
      let es := source[i];
      let source := source.set i AssocList.nil h;
      let target := AssocList.foldl (reinsertAux hash) target es;
      go (i + 1) source target
    else target) =
    target
-- Mathlib/Order/Filter/Prod.lean
theorem mem_prod_top {s : Set (α × β)} :
    s ∈ f ×ˢ (⊤ : Filter β) ↔ { a | ∀ b, (a, b) ∈ s } ∈ f

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
s : Set (α × β)
⊢ {a | ∀ b ∈ univ, (a, b) ∈ s} ∈ f ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f

Tactic:
simp only [mem_univ, forall_true_left]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
s : Set (α × β)
⊢ s ∈ f ×ˢ ⊤ ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f

Tactic:
rw [← principal_univ, mem_prod_principal]

Result:
α : Type u_1
β : Type u_2
f : Filter α
s : Set (α × β)
⊢ {a | ∀ b ∈ univ, (a, b) ∈ s} ∈ f ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f
-- Mathlib/Control/EquivFunctor.lean
theorem mapEquiv_refl (α) : mapEquiv f (Equiv.refl α) = Equiv.refl (f α)

Proof state:
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α : Type u₀
⊢ mapEquiv f (Equiv.refl α) = Equiv.refl (f α)

Tactic:
ext

Result:
case H
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α : Type u₀
x✝ : f α
⊢ (mapEquiv f (Equiv.refl α)) x✝ = (Equiv.refl (f α)) x✝

Proof state:
case H
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α : Type u₀
x✝ : f α
⊢ (mapEquiv f (Equiv.refl α)) x✝ = (Equiv.refl (f α)) x✝

Tactic:
simp [mapEquiv]

Result:
no goals
-- Mathlib/Data/Int/LeastGreatest.lean
theorem coe_greatestOfBdd_eq {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ}
    (Hb : ∀ z : ℤ, P z → z ≤ b) (Hb' : ∀ z : ℤ, P z → z ≤ b') (Hinh : ∃ z : ℤ, P z) :
    (greatestOfBdd b Hb Hinh : ℤ) = greatestOfBdd b' Hb' Hinh

Proof state:
case mk.intro.mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → z ≤ n
n' : ℤ
hn' : P n'
h2n' : ∀ (z : ℤ), P z → z ≤ n'
⊢ ↑⟨n, ⋯⟩ = ↑⟨n', ⋯⟩

Tactic:
exact le_antisymm (h2n' _ hn) (h2n _ hn')

Result:
no goals

Proof state:
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ z, P z
⊢ ↑(b.greatestOfBdd Hb Hinh) = ↑(b'.greatestOfBdd Hb' Hinh)

Tactic:
rcases greatestOfBdd b Hb Hinh with ⟨n, hn, h2n⟩

Result:
case mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → z ≤ n
⊢ ↑⟨n, ⋯⟩ = ↑(b'.greatestOfBdd Hb' Hinh)

Proof state:
case mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → z ≤ n
⊢ ↑⟨n, ⋯⟩ = ↑(b'.greatestOfBdd Hb' Hinh)

Tactic:
rcases greatestOfBdd b' Hb' Hinh with ⟨n', hn', h2n'⟩

Result:
case mk.intro.mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → z ≤ n
n' : ℤ
hn' : P n'
h2n' : ∀ (z : ℤ), P z → z ≤ n'
⊢ ↑⟨n, ⋯⟩ = ↑⟨n', ⋯⟩