harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Colimit/Ring.lean
theorem of.zero_exact {i x} (hix : of G (f' · · ·) i x = 0) :
    ∃ (j : _) (hij : i ≤ j), f' i j hij x = 0

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : DirectedSystem G fun i j h => ⇑(f' i j h)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x : G i
hix : (of G (fun x1 x2 x3 => ⇑(f' x1 x2 x3)) i) x = 0
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0

Tactic:
have := Nonempty.intro i

Result:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : DirectedSystem G fun i j h => ⇑(f' i j h)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x : G i
hix : (of G (fun x1 x2 x3 => ⇑(f' x1 x2 x3)) i) x = 0
this : Nonempty ι
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : DirectedSystem G fun i j h => ⇑(f' i j h)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x : G i
this : Nonempty ι
hix : (ringEquiv G f') ((of G (fun x1 x2 x3 => ⇑(f' x1 x2 x3)) i) x) = (ringEquiv G f') 0
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0

Tactic:
rwa [map_zero, ringEquiv_of, DirectLimit.exists_eq_zero] at hix

Result:
no goals

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : DirectedSystem G fun i j h => ⇑(f' i j h)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x : G i
hix : (of G (fun x1 x2 x3 => ⇑(f' x1 x2 x3)) i) x = 0
this : Nonempty ι
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0

Tactic:
apply_fun ringEquiv _ _ at hix

Result:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : DirectedSystem G fun i j h => ⇑(f' i j h)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x : G i
this : Nonempty ι
hix : (ringEquiv G f') ((of G (fun x1 x2 x3 => ⇑(f' x1 x2 x3)) i) x) = (ringEquiv G f') 0
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_extend_one_subset {f : α → M'} {g : α → N} :
    mulSupport (f.extend g 1) ⊆ f '' mulSupport g :=
  mulSupport_subset_iff'.mpr fun x hfg ↦ by
    by_cases hf : ∃ a, f a = x
    · rw [extend, dif_pos hf, ← nmem_mulSupport]
      rw [← Classical.choose_spec hf] at hfg
      exact fun hg ↦ hfg ⟨_, hg, rfl⟩
    · rw [extend_apply' _ _ _ hf]; rfl

Proof state:
case neg
α : Type u_1
M' : Type u_6
N : Type u_7
inst✝ : One N
f : α → M'
g : α → N
x : M'
hfg : x ∉ f '' mulSupport g
hf : ¬∃ a, f a = x
⊢ extend f g 1 x = 1

Tactic:
rw [extend_apply' _ _ _ hf]

Result:
case neg
α : Type u_1
M' : Type u_6
N : Type u_7
inst✝ : One N
f : α → M'
g : α → N
x : M'
hfg : x ∉ f '' mulSupport g
hf : ¬∃ a, f a = x
⊢ 1 x = 1

Proof state:
case pos
α : Type u_1
M' : Type u_6
N : Type u_7
inst✝ : One N
f : α → M'
g : α → N
x : M'
hfg : x ∉ f '' mulSupport g
hf : ∃ a, f a = x
⊢ extend f g 1 x = 1

Tactic:
rw [extend, dif_pos hf, ← nmem_mulSupport]

Result:
case pos
α : Type u_1
M' : Type u_6
N : Type u_7
inst✝ : One N
f : α → M'
g : α → N
x : M'
hfg : x ∉ f '' mulSupport g
hf : ∃ a, f a = x
⊢ Classical.choose hf ∉ mulSupport g

Proof state:
case neg
α : Type u_1
M' : Type u_6
N : Type u_7
inst✝ : One N
f : α → M'
g : α → N
x : M'
hfg : x ∉ f '' mulSupport g
hf : ¬∃ a, f a = x
⊢ 1 x = 1

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
M' : Type u_6
N : Type u_7
inst✝ : One N
f : α → M'
g : α → N
x : M'
hfg : x ∉ f '' mulSupport g
hf : ∃ a, f a = x
⊢ Classical.choose hf ∉ mulSupport g

Tactic:
rw [← Classical.choose_spec hf] at hfg

Result:
case pos
α : Type u_1
M' : Type u_6
N : Type u_7
inst✝ : One N
f : α → M'
g : α → N
x : M'
hf : ∃ a, f a = x
hfg : f (Classical.choose hf) ∉ f '' mulSupport g
⊢ Classical.choose hf ∉ mulSupport g

Proof state:
case pos
α : Type u_1
M' : Type u_6
N : Type u_7
inst✝ : One N
f : α → M'
g : α → N
x : M'
hf : ∃ a, f a = x
hfg : f (Classical.choose hf) ∉ f '' mulSupport g
⊢ Classical.choose hf ∉ mulSupport g

Tactic:
exact fun hg ↦ hfg ⟨_, hg, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
M' : Type u_6
N : Type u_7
inst✝ : One N
f : α → M'
g : α → N
x : M'
hfg : x ∉ f '' mulSupport g
⊢ extend f g 1 x = 1

Tactic:
by_cases hf : ∃ a, f a = x

Result:
case pos
α : Type u_1
M' : Type u_6
N : Type u_7
inst✝ : One N
f : α → M'
g : α → N
x : M'
hfg : x ∉ f '' mulSupport g
hf : ∃ a, f a = x
⊢ extend f g 1 x = 1

case neg
α : Type u_1
M' : Type u_6
N : Type u_7
inst✝ : One N
f : α → M'
g : α → N
x : M'
hfg : x ∉ f '' mulSupport g
hf : ¬∃ a, f a = x
⊢ extend f g 1 x = 1
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem tendsto_pow_atTop_nhds_zero_of_lt_one {𝕜 : Type*} [LinearOrderedField 𝕜] [Archimedean 𝕜]
    [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 ≤ r) (h₂ : r < 1) :
    Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0) :=
  h₁.eq_or_lt.elim
    (fun hr ↦ (tendsto_add_atTop_iff_nat 1).mp <| by
      simp [_root_.pow_succ, ← hr, tendsto_const_nhds])
    (fun hr ↦
      have := (one_lt_inv₀ hr).2 h₂ |> tendsto_pow_atTop_atTop_of_one_lt
      (tendsto_inv_atTop_zero.comp this).congr fun n ↦ by simp)

Proof state:
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h₁ : 0 ≤ r
h₂ : r < 1
hr : 0 < r
this : Tendsto (fun n => r⁻¹ ^ n) atTop atTop
n : ℕ
⊢ ((fun r => r⁻¹) ∘ fun n => r⁻¹ ^ n) n = r ^ n

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h₁ : 0 ≤ r
h₂ : r < 1
hr : 0 = r
⊢ Tendsto (fun n => r ^ (n + 1)) atTop (𝓝 0)

Tactic:
simp [_root_.pow_succ, ← hr, tendsto_const_nhds]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem exists_multiset_of_mem_closure {M : Type*} [CommMonoid M] {s : Set M} {x : M}
    (hx : x ∈ closure s) : ∃ l : Multiset M, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Proof state:
case intro.intro
M : Type u_4
inst✝ : CommMonoid M
s : Set M
x : M
hx : x ∈ closure s
l : List M
h1 : ∀ y ∈ l, y ∈ s
h2 : l.prod = x
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
exact ⟨l, h1, (Multiset.prod_coe l).trans h2⟩

Result:
no goals

Proof state:
M : Type u_4
inst✝ : CommMonoid M
s : Set M
x : M
hx : x ∈ closure s
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
obtain ⟨l, h1, h2⟩ := exists_list_of_mem_closure hx

Result:
case intro.intro
M : Type u_4
inst✝ : CommMonoid M
s : Set M
x : M
hx : x ∈ closure s
l : List M
h1 : ∀ y ∈ l, y ∈ s
h2 : l.prod = x
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x
-- Mathlib/RingTheory/Localization/Cardinality.lean
theorem cardinalMk {S : Submonoid R} (hS : S ≤ R⁰) : #(Localization S) = #R

Proof state:
case h.e'_4
R : Type u
inst✝ : CommRing R
S : Submonoid R
hS : S ≤ R⁰
⊢ nonZeroDivisorsRight R = R⁰

Tactic:
ext x

Result:
case h.e'_4.h
R : Type u
inst✝ : CommRing R
S : Submonoid R
hS : S ≤ R⁰
x : R
⊢ x ∈ nonZeroDivisorsRight R ↔ x ∈ R⁰

Proof state:
case hS
R : Type u
inst✝ : CommRing R
S : Submonoid R
hS : S ≤ R⁰
⊢ S ≤ nonZeroDivisorsRight R

Tactic:
convert hS using 1

Result:
case h.e'_4
R : Type u
inst✝ : CommRing R
S : Submonoid R
hS : S ≤ R⁰
⊢ nonZeroDivisorsRight R = R⁰

Proof state:
case h.e'_4.h
R : Type u
inst✝ : CommRing R
S : Submonoid R
hS : S ≤ R⁰
x : R
⊢ x ∈ nonZeroDivisorsRight R ↔ x ∈ R⁰

Tactic:
rw [mem_nonZeroDivisorsRight_iff, mem_nonZeroDivisors_iff]

Result:
case h.e'_4.h
R : Type u
inst✝ : CommRing R
S : Submonoid R
hS : S ≤ R⁰
x : R
⊢ (∀ (y : R), x * y = 0 → y = 0) ↔ ∀ (x_1 : R), x_1 * x = 0 → x_1 = 0

Proof state:
case h.e'_4.h
R : Type u
inst✝ : CommRing R
S : Submonoid R
hS : S ≤ R⁰
x : R
⊢ (∀ (y : R), x * y = 0 → y = 0) ↔ ∀ (x_1 : R), x_1 * x = 0 → x_1 = 0

Tactic:
congr! 3

Result:
case h.e'_4.h.a.h.h.h.e'_2
R : Type u
inst✝ : CommRing R
S : Submonoid R
hS : S ≤ R⁰
x a✝ : R
⊢ x * a✝ = a✝ * x

Proof state:
case h.e'_4.h.a.h.h.h.e'_2
R : Type u
inst✝ : CommRing R
S : Submonoid R
hS : S ≤ R⁰
x a✝ : R
⊢ x * a✝ = a✝ * x

Tactic:
rw [mul_comm]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
S : Submonoid R
hS : S ≤ R⁰
⊢ #(Localization S) = #R

Tactic:
apply OreLocalization.cardinalMk

Result:
case hS
R : Type u
inst✝ : CommRing R
S : Submonoid R
hS : S ≤ R⁰
⊢ S ≤ nonZeroDivisorsRight R
-- Mathlib/Data/DFinsupp/Order.lean
theorem subset_support_tsub : f.support \ g.support ⊆ (f - g).support

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (α i)
inst✝⁵ : (i : ι) → PartialOrder (α i)
inst✝⁴ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝³ : (i : ι) → Sub (α i)
inst✝² : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ f.support \ g.support ⊆ (f - g).support

Tactic:
simp +contextual [subset_iff]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem swapCore_comm (r a b : α) : swapCore a b r = swapCore b a r

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ swapCore a b r = swapCore b a r

Tactic:
unfold swapCore

Result:
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r

Tactic:
split_ifs <;> cc

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
@[simp] lemma dens_empty : dens (∅ : Finset α) = 0

Proof state:
α : Type u_2
inst✝ : Fintype α
⊢ ∅.dens = 0

Tactic:
simp [dens]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofNat_toNat (m : Nat) (x : BitVec n) : BitVec.ofNat m x.toNat = setWidth m x

Proof state:
n m : Nat
x : BitVec n
⊢ BitVec.ofNat m x.toNat = setWidth m x

Tactic:
apply eq_of_toNat_eq

Result:
case a
n m : Nat
x : BitVec n
⊢ (BitVec.ofNat m x.toNat).toNat = (setWidth m x).toNat

Proof state:
case a
n m : Nat
x : BitVec n
⊢ (BitVec.ofNat m x.toNat).toNat = (setWidth m x).toNat

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem prod_cyclotomic'_eq_X_pow_sub_one {K : Type*} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ}
    (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) :
    ∏ i ∈ Nat.divisors n, cyclotomic' i K = X ^ n - 1

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hd : (↑n.divisors).PairwiseDisjoint fun k => primitiveRoots k K
⊢ ∏ i ∈ n.divisors, cyclotomic' i K = X ^ n - 1

Tactic:
simp only [X_pow_sub_one_eq_prod hpos h, cyclotomic', ← Finset.prod_biUnion hd,
  IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots]

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ ∏ i ∈ n.divisors, cyclotomic' i K = X ^ n - 1

Tactic:
classical
have hd : (n.divisors : Set ℕ).PairwiseDisjoint fun k => primitiveRoots k K :=
  fun x _ y _ hne => IsPrimitiveRoot.disjoint hne
simp only [X_pow_sub_one_eq_prod hpos h, cyclotomic', ← Finset.prod_biUnion hd,
  IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots]

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ ∏ i ∈ n.divisors, cyclotomic' i K = X ^ n - 1

Tactic:
have hd : (n.divisors : Set ℕ).PairwiseDisjoint fun k => primitiveRoots k K :=
  fun x _ y _ hne => IsPrimitiveRoot.disjoint hne

Result:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hd : (↑n.divisors).PairwiseDisjoint fun k => primitiveRoots k K
⊢ ∏ i ∈ n.divisors, cyclotomic' i K = X ^ n - 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_eq_false_distrib : ∀(c t f : Bool),
    (cond c t f = false) = ite (c = true) (t = false) (f = false)

Proof state:
⊢ ∀ (c t f : Bool), ((bif c then t else f) = false) = if c = true then t = false else f = false

Tactic:
decide

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem map_subset_iff {l₁ l₂ : List α} (f : α → β) (h : Injective f) :
    map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂

Proof state:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
⊢ x ∈ l₂

Tactic:
rcases mem_map.1 (h2 (mem_map_of_mem f hx)) with ⟨x', hx', hxx'⟩

Result:
case intro.intro
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
x' : α
hx' : x' ∈ l₂
hxx' : f x' = f x
⊢ x ∈ l₂

Proof state:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ → l₁ ⊆ l₂

Tactic:
intro h2 x hx

Result:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
⊢ x ∈ l₂

Proof state:
case intro.intro
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
x' : α
hx' : x' ∈ l₂
hxx' : f x' = f x
⊢ x ∈ l₂

Tactic:
cases h hxx'

Result:
case intro.intro.refl
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
hx' : x ∈ l₂
hxx' : f x = f x
⊢ x ∈ l₂

Proof state:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂

Tactic:
refine ⟨?_, map_subset f⟩

Result:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ → l₁ ⊆ l₂

Proof state:
case intro.intro.refl
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
hx' : x ∈ l₂
hxx' : f x = f x
⊢ x ∈ l₂

Tactic:
exact hx'

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem finrank_euclideanSpace :
    Module.finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : Fintype ι
⊢ Module.finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι

Tactic:
simp [EuclideanSpace, PiLp, WithLp]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem IsTheta.comp_fst : f =Θ[l] g → (f ∘ Prod.fst) =Θ[l ×ˢ l'] (g ∘ Prod.fst)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g ∧ g =O[l] f → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst) ∧ (g ∘ Prod.fst) =O[l ×ˢ l'] (f ∘ Prod.fst)

Tactic:
exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.comp_fst l', h₂.comp_fst l'⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =Θ[l] g → (f ∘ Prod.fst) =Θ[l ×ˢ l'] (g ∘ Prod.fst)

Tactic:
simp only [IsTheta, eventually_and]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g ∧ g =O[l] f → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst) ∧ (g ∘ Prod.fst) =O[l ×ˢ l'] (f ∘ Prod.fst)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem get_attach {o : Option α} (h : o.attach.isSome = true) :
    o.attach.get h = ⟨o.get (by simpa using h), by simp⟩

Proof state:
case some
α : Type u_1
val✝ : α
h : (some val✝).attach.isSome = true
⊢ (some val✝).attach.get h = ⟨(some val✝).get ⋯, ⋯⟩

Tactic:
simp [get_some]

Result:
no goals

Proof state:
case none
α : Type u_1
h : none.attach.isSome = true
⊢ none.attach.get h = ⟨none.get ⋯, ⋯⟩

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type ?u.6578
o : Option α
h : o.attach.isSome = true
⊢ o.get ⋯ ∈ o

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.6578
o : Option α
h : o.attach.isSome = true
⊢ o.isSome = true

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
o : Option α
h : o.attach.isSome = true
⊢ o.attach.get h = ⟨o.get ⋯, ⋯⟩

Tactic:
cases o

Result:
case none
α : Type u_1
h : none.attach.isSome = true
⊢ none.attach.get h = ⟨none.get ⋯, ⋯⟩

case some
α : Type u_1
val✝ : α
h : (some val✝).attach.isSome = true
⊢ (some val✝).attach.get h = ⟨(some val✝).get ⋯, ⋯⟩
-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive le_card_add_mul_addEnergy] lemma le_card_add_mul_mulEnergy (s t : Finset α) :
    s.card ^ 2 * t.card ^ 2 ≤ (s * t).card * Eₘ[s, t] :=
  calc
    _ = ((s ×ˢ t).filter fun (a, b) ↦ a * b ∈ s * t).card ^ 2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #s ^ 2 * #t ^ 2 =
    #(filter
          (fun x =>
            match x with
            | (a, b) => a * b ∈ s * t)
          (s ×ˢ t)) ^
      2

Tactic:
rw [filter_eq_self.2, card_product, mul_pow]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ ∀ x ∈ s ×ˢ t,
    match x with
    | (a, b) => a * b ∈ s * t

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ ∀ x ∈ s ×ˢ t,
    match x with
    | (a, b) => a * b ∈ s * t

Tactic:
aesop (add unsafe mul_mem_mul)

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem sSameSide_iff_exists_right {s : AffineSubspace R P} {x y p₂ : P} (h : p₂ ∈ s) :
    s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
⊢ (x ∉ s ∧ y ∉ s ∧ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔
    x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
simp_rw [SameRay.sameRay_comm]

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
⊢ s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
rw [sSameSide_comm, sSameSide_iff_exists_left h, ← and_assoc, and_comm (a := y ∉ s), and_assoc]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
⊢ (x ∉ s ∧ y ∉ s ∧ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔
    x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_restrictVarLeft [DecidableEq α] {γ : Type*} {t : L.Term (α ⊕ γ)}
    {f : t.varFinsetLeft → β}
    {xs : β ⊕ γ → M} (xs' : α → M) (hxs' : ∀ a, xs (Sum.inl (f a)) = xs' a) :
    (t.restrictVarLeft f).realize xs = t.realize (Sum.elim xs' (xs ∘ Sum.inr))

Proof state:
case var
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
a : α ⊕ γ
f : { x // x ∈ (var a).varFinsetLeft } → β
hxs' : ∀ (a_1 : { x // x ∈ (var a).varFinsetLeft }), xs (Sum.inl (f a_1)) = xs' ↑a_1
⊢ realize xs ((var a).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (var a)

Tactic:
cases a <;> simp [restrictVarLeft, hxs']

Result:
no goals

Proof state:
case func
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term (α ⊕ γ)
ih :
  ∀ (a : Fin l✝) {f : { x // x ∈ (_ts✝ a).varFinsetLeft } → β},
    (∀ (a_1 : { x // x ∈ (_ts✝ a).varFinsetLeft }), xs (Sum.inl (f a_1)) = xs' ↑a_1) →
      realize xs ((_ts✝ a).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (_ts✝ a)
f : { x // x ∈ (func _f✝ _ts✝).varFinsetLeft } → β
hxs' : ∀ (a : { x // x ∈ (func _f✝ _ts✝).varFinsetLeft }), xs (Sum.inl (f a)) = xs' ↑a
⊢ realize xs ((func _f✝ _ts✝).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (func _f✝ _ts✝)

Tactic:
exact congr rfl (funext fun i => ih i (by simp [hxs']))

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term (α ⊕ γ)
ih :
  ∀ (a : Fin l✝) {f : { x // x ∈ (_ts✝ a).varFinsetLeft } → β},
    (∀ (a_1 : { x // x ∈ (_ts✝ a).varFinsetLeft }), xs (Sum.inl (f a_1)) = xs' ↑a_1) →
      realize xs ((_ts✝ a).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (_ts✝ a)
f : { x // x ∈ (func _f✝ _ts✝).varFinsetLeft } → β
hxs' : ∀ (a : { x // x ∈ (func _f✝ _ts✝).varFinsetLeft }), xs (Sum.inl (f a)) = xs' ↑a
i : Fin l✝
⊢ ∀ (a : { x // x ∈ (_ts✝ i).varFinsetLeft }), xs (Sum.inl ((f ∘ Set.inclusion ⋯) a)) = xs' ↑a

Tactic:
simp [hxs']

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_4
t : L.Term (α ⊕ γ)
f : { x // x ∈ t.varFinsetLeft } → β
xs : β ⊕ γ → M
xs' : α → M
hxs' : ∀ (a : { x // x ∈ t.varFinsetLeft }), xs (Sum.inl (f a)) = xs' ↑a
⊢ realize xs (t.restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) t

Tactic:
induction t with
| var a => cases a <;> simp [restrictVarLeft, hxs']
| func _ _ ih =>
  exact congr rfl (funext fun i => ih i (by simp [hxs']))

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem toReal_sub_of_le {a b : ℝ≥0∞} (h : b ≤ a) (ha : a ≠ ∞) :
    (a - b).toReal = a.toReal - b.toReal

Proof state:
a b : ℝ≥0∞
h : b ≤ a
ha : a ≠ ⊤
⊢ (a - b).toReal = a.toReal - b.toReal

Tactic:
lift b to ℝ≥0 using ne_top_of_le_ne_top ha h

Result:
case intro
a : ℝ≥0∞
ha : a ≠ ⊤
b : ℝ≥0
h : ↑b ≤ a
⊢ (a - ↑b).toReal = a.toReal - (↑b).toReal

Proof state:
case intro.intro
b a : ℝ≥0
h : ↑b ≤ ↑a
⊢ (↑a - ↑b).toReal = (↑a).toReal - (↑b).toReal

Tactic:
simp only [← ENNReal.coe_sub, ENNReal.coe_toReal, NNReal.coe_sub (ENNReal.coe_le_coe.mp h)]

Result:
no goals

Proof state:
case intro
a : ℝ≥0∞
ha : a ≠ ⊤
b : ℝ≥0
h : ↑b ≤ a
⊢ (a - ↑b).toReal = a.toReal - (↑b).toReal

Tactic:
lift a to ℝ≥0 using ha

Result:
case intro.intro
b a : ℝ≥0
h : ↑b ≤ ↑a
⊢ (↑a - ↑b).toReal = (↑a).toReal - (↑b).toReal
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem findSome?_subtype {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.findSome? f = l.unattach.findSome? g

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : findSome? f l = findSome? g (map (fun x => x.val) l)
⊢ findSome? f (a :: l) = findSome? g (map (fun x => x.val) (a :: l))

Tactic:
simp [ih, hf, findSome?_cons]

Result:
no goals

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

Tactic:
unfold unattach

Result:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findSome? f l = findSome? g (map (fun x => x.val) l)

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findSome? f l = findSome? g (map (fun x => x.val) l)

Tactic:
induction l with
| nil => simp
| cons a l ih => simp [ih, hf, findSome?_cons]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findSome? f [] = findSome? g (map (fun x => x.val) [])

Tactic:
simp

Result:
no goals