harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem not_isOfFinOrder_of_injective_pow {x : G} (h : Injective fun n : ℕ => x ^ n) :
    ¬IsOfFinOrder x

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n => x ^ n
⊢ ¬IsOfFinOrder x

Tactic:
simp_rw [isOfFinOrder_iff_pow_eq_one, not_exists, not_and]

Result:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n => x ^ n
⊢ ∀ (x_1 : ℕ), 0 < x_1 → ¬x ^ x_1 = 1

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n => x ^ n
⊢ ∀ (x_1 : ℕ), 0 < x_1 → ¬x ^ x_1 = 1

Tactic:
intro n hn_pos hnx

Result:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = 1
⊢ False

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = x ^ 0
⊢ False

Tactic:
rw [h hnx] at hn_pos

Result:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < 0
hnx : x ^ n = x ^ 0
⊢ False

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < 0
hnx : x ^ n = x ^ 0
⊢ False

Tactic:
exact irrefl 0 hn_pos

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = 1
⊢ False

Tactic:
rw [← pow_zero x] at hnx

Result:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = x ^ 0
⊢ False
-- Mathlib/Algebra/Ring/Int/Units.lean
lemma units_ne_iff_eq_neg {u v : ℤˣ} : u ≠ v ↔ u = -v

Proof state:
u v : ℤˣ
⊢ u ≠ v ↔ u = -v

Tactic:
simpa only [Ne, Units.ext_iff] using isUnit_ne_iff_eq_neg u.isUnit v.isUnit

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem _root_.Real.toNNReal_rpow_of_nonneg {x y : ℝ} (hx : 0 ≤ x) :
    Real.toNNReal (x ^ y) = Real.toNNReal x ^ y

Proof state:
x y : ℝ
hx : 0 ≤ x
⊢ (x ^ y).toNNReal = x.toNNReal ^ y

Tactic:
nth_rw 1 [← Real.coe_toNNReal x hx]

Result:
x y : ℝ
hx : 0 ≤ x
⊢ (↑x.toNNReal ^ y).toNNReal = x.toNNReal ^ y

Proof state:
x y : ℝ
hx : 0 ≤ x
⊢ (↑x.toNNReal ^ y).toNNReal = x.toNNReal ^ y

Tactic:
rw [← NNReal.coe_rpow, Real.toNNReal_coe]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem pos_iff_one_le {x : PartENat} : 0 < x ↔ 1 ≤ x :=
  PartENat.casesOn x
    (by simp only [le_top, natCast_lt_top, ← @Nat.cast_zero PartENat])
    fun n => by
      rw [← Nat.cast_zero, ← Nat.cast_one, PartENat.coe_lt_coe, PartENat.coe_le_coe]
      rfl

Proof state:
x : PartENat
⊢ 0 < ⊤ ↔ 1 ≤ ⊤

Tactic:
simp only [le_top, natCast_lt_top, ← @Nat.cast_zero PartENat]

Result:
no goals

Proof state:
x : PartENat
n : ℕ
⊢ 0 < ↑n ↔ 1 ≤ ↑n

Tactic:
rw [← Nat.cast_zero, ← Nat.cast_one, PartENat.coe_lt_coe, PartENat.coe_le_coe]

Result:
x : PartENat
n : ℕ
⊢ 0 < n ↔ 1 ≤ n

Proof state:
x : PartENat
n : ℕ
⊢ 0 < n ↔ 1 ≤ n

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Ab.lean
lemma exact_iff_surjective_abToCycles :
    S.Exact ↔ Function.Surjective S.abToCycles

Proof state:
S : ShortComplex Ab
⊢ Function.Surjective ⇑(ConcreteCategory.hom (AddCommGrp.ofHom S.abToCycles)) ↔ Function.Surjective ⇑S.abToCycles

Tactic:
rfl

Result:
no goals

Proof state:
S : ShortComplex Ab
⊢ S.Exact ↔ Function.Surjective ⇑S.abToCycles

Tactic:
rw [S.abLeftHomologyData.exact_iff_epi_f', abLeftHomologyData_f',
  AddCommGrp.epi_iff_surjective]

Result:
S : ShortComplex Ab
⊢ Function.Surjective ⇑(ConcreteCategory.hom (AddCommGrp.ofHom S.abToCycles)) ↔ Function.Surjective ⇑S.abToCycles
-- Mathlib/Data/List/Sym.lean
theorem length_sym {n : ℕ} {xs : List α} :
    (xs.sym n).length = Nat.multichoose xs.length n :=
  match n, xs with
  | 0, _ => by rw [List.sym, Nat.multichoose]; rfl
  | n + 1, [] => by simp [List.sym]
  | n + 1, x :: xs => by
    rw [List.sym, length_append, length_map, length_cons]
    rw [@length_sym n (x :: xs), @length_sym (n + 1) xs]
    rw [Nat.multichoose_succ_succ, length_cons, add_comm]

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (List.sym (n + 1) (x :: xs)).length = (x :: xs).length.multichoose (n + 1)

Tactic:
rw [List.sym, length_append, length_map, length_cons]

Result:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (List.sym n (x :: xs)).length + (List.sym (n + 1) xs).length = (xs.length + 1).multichoose (n + 1)

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (List.sym n (x :: xs)).length + (List.sym (n + 1) xs).length = (xs.length + 1).multichoose (n + 1)

Tactic:
rw [@length_sym n (x :: xs), @length_sym (n + 1) xs]

Result:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) = (xs.length + 1).multichoose (n + 1)

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) = (xs.length + 1).multichoose (n + 1)

Tactic:
rw [Nat.multichoose_succ_succ, length_cons, add_comm]

Result:
no goals

Proof state:
α : Type u_1
n✝ : ℕ
xs : List α
n : ℕ
⊢ (List.sym (n + 1) []).length = [].length.multichoose (n + 1)

Tactic:
simp [List.sym]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
xs x✝ : List α
⊢ (List.sym 0 x✝).length = x✝.length.multichoose 0

Tactic:
rw [List.sym, Nat.multichoose]

Result:
α : Type u_1
n : ℕ
xs x✝ : List α
⊢ [Sym.nil].length = 1

Proof state:
α : Type u_1
n : ℕ
xs x✝ : List α
⊢ [Sym.nil].length = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Basic.lean
lemma ltTrichotomy_eq_iff : ltTrichotomy x y p q r = s ↔
    (x < y ∧ p = s) ∨ (x = y ∧ q = s) ∨ (y < x ∧ r = s)

Proof state:
case refine_1
α : Type u_2
inst✝ : LinearOrder α
P : Sort u_5
x y : α
p q r s : P
h : x < y
⊢ ltTrichotomy x y p q r = s ↔ x < y ∧ p = s ∨ x = y ∧ q = s ∨ y < x ∧ r = s

Tactic:
simp only [ltTrichotomy_lt, false_and, true_and, or_false, h, h.not_lt, h.ne]

Result:
no goals

Proof state:
case refine_2
α : Type u_2
inst✝ : LinearOrder α
P : Sort u_5
x y : α
p q r s : P
h : x = y
⊢ ltTrichotomy x y p q r = s ↔ x < y ∧ p = s ∨ x = y ∧ q = s ∨ y < x ∧ r = s

Tactic:
simp only [ltTrichotomy_eq, false_and, true_and, or_false, false_or, h, lt_irrefl]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
P : Sort u_5
x y : α
p q r s : P
⊢ ltTrichotomy x y p q r = s ↔ x < y ∧ p = s ∨ x = y ∧ q = s ∨ y < x ∧ r = s

Tactic:
refine ltByCases x y (fun h => ?_) (fun h => ?_) (fun h => ?_)

Result:
case refine_1
α : Type u_2
inst✝ : LinearOrder α
P : Sort u_5
x y : α
p q r s : P
h : x < y
⊢ ltTrichotomy x y p q r = s ↔ x < y ∧ p = s ∨ x = y ∧ q = s ∨ y < x ∧ r = s

case refine_2
α : Type u_2
inst✝ : LinearOrder α
P : Sort u_5
x y : α
p q r s : P
h : x = y
⊢ ltTrichotomy x y p q r = s ↔ x < y ∧ p = s ∨ x = y ∧ q = s ∨ y < x ∧ r = s

case refine_3
α : Type u_2
inst✝ : LinearOrder α
P : Sort u_5
x y : α
p q r s : P
h : y < x
⊢ ltTrichotomy x y p q r = s ↔ x < y ∧ p = s ∨ x = y ∧ q = s ∨ y < x ∧ r = s

Proof state:
case refine_3
α : Type u_2
inst✝ : LinearOrder α
P : Sort u_5
x y : α
p q r s : P
h : y < x
⊢ ltTrichotomy x y p q r = s ↔ x < y ∧ p = s ∨ x = y ∧ q = s ∨ y < x ∧ r = s

Tactic:
simp only [ltTrichotomy_gt, false_and, true_and, false_or, h, h.not_lt, h.ne']

Result:
no goals
-- Mathlib/Topology/Bornology/Hom.lean
theorem cancel_left {g : LocallyBoundedMap β γ} {f₁ f₂ : LocallyBoundedMap α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : Bornology γ
g : LocallyBoundedMap β γ
f₁ f₂ : LocallyBoundedMap α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem OrderEmbedding.image_Ioi (e : α ↪o β) (he : IsUpperSet (range e)) (a : α) :
    e '' Ioi a = Ioi (e a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : IsUpperSet (range ⇑e)
a : α
⊢ ⇑e '' Ioi a = Ioi (e a)

Tactic:
rw [← e.preimage_Ioi, image_preimage_eq_inter_range,
  inter_eq_left.2 <| he.Ioi_subset (mem_range_self _)]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem coeff_map (p : MvPolynomial σ R) : ∀ m : σ →₀ ℕ, coeff m (map f p) = f (coeff m p)

Proof state:
case h_add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p q : MvPolynomial σ R
hp : ∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)
hq : ∀ (m : σ →₀ ℕ), coeff m ((map f) q) = f (coeff m q)
m : σ →₀ ℕ
⊢ coeff m ((map f) (p + q)) = f (coeff m (p + q))

Tactic:
simp only [hp, hq, (map f).map_add, coeff_add]

Result:
case h_add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p q : MvPolynomial σ R
hp : ∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)
hq : ∀ (m : σ →₀ ℕ), coeff m ((map f) q) = f (coeff m q)
m : σ →₀ ℕ
⊢ f (coeff m p) + f (coeff m q) = f (coeff m p + coeff m q)
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
/-- Pajor's variant of the **Sauer-Shelah lemma**. -/
lemma card_le_card_shatterer (𝒜 : Finset (Finset α)) : #𝒜 ≤ #𝒜.shatterer

Proof state:
case refine_3.inl
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters (insert a s)
⊢ False

Tactic:
exact aux (fun t ht ↦ (mem_memberSubfamily.1 ht).2) hs <| mem_insert_self _ _

Result:
no goals

Proof state:
case refine_3.refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
⊢ (memberSubfamily a 𝒜).shatterer ⊆ 𝒜.shatterer

Tactic:
simp only [subset_iff, mem_shatterer]

Result:
case refine_3.refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
⊢ ∀ ⦃x : Finset α⦄, (memberSubfamily a 𝒜).Shatters x → 𝒜.Shatters x
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_def (x : PGame) :
    birthday x =
      max (lsub.{u, u} fun i => birthday (x.moveLeft i))
        (lsub.{u, u} fun i => birthday (x.moveRight i))

Proof state:
case mk
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (mk α✝ β✝ a✝¹ a✝).birthday =
    (lsub fun i => ((mk α✝ β✝ a✝¹ a✝).moveLeft i).birthday) ⊔ lsub fun i => ((mk α✝ β✝ a✝¹ a✝).moveRight i).birthday

Tactic:
rw [birthday]

Result:
case mk
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ((lsub fun i => (a✝¹ i).birthday) ⊔ lsub fun i => (a✝ i).birthday) =
    (lsub fun i => ((mk α✝ β✝ a✝¹ a✝).moveLeft i).birthday) ⊔ lsub fun i => ((mk α✝ β✝ a✝¹ a✝).moveRight i).birthday

Proof state:
case mk
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ((lsub fun i => (a✝¹ i).birthday) ⊔ lsub fun i => (a✝ i).birthday) =
    (lsub fun i => ((mk α✝ β✝ a✝¹ a✝).moveLeft i).birthday) ⊔ lsub fun i => ((mk α✝ β✝ a✝¹ a✝).moveRight i).birthday

Tactic:
rfl

Result:
no goals

Proof state:
x : PGame
⊢ x.birthday = (lsub fun i => (x.moveLeft i).birthday) ⊔ lsub fun i => (x.moveRight i).birthday

Tactic:
cases x

Result:
case mk
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (mk α✝ β✝ a✝¹ a✝).birthday =
    (lsub fun i => ((mk α✝ β✝ a✝¹ a✝).moveLeft i).birthday) ⊔ lsub fun i => ((mk α✝ β✝ a✝¹ a✝).moveRight i).birthday
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
    (h : m.WF) (h₁ : k ∉ m) (h₂ : (f (m.get? k)).isSome) :
    (m.alter k f).size = m.size + 1

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
h₁ : ¬k ∈ m
h₂ : (f (m.get? k)).isSome = true
⊢ (m.alter k f).size = m.size + 1

Tactic:
revert h₁ h₂

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ ¬k ∈ m → (f (m.get? k)).isSome = true → (m.alter k f).size = m.size + 1

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ ¬k ∈ m → (f (m.get? k)).isSome = true → (m.alter k f).size = m.size + 1

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ m.contains k = false → (f (m.get? k)).isSome = true → (m.alter k f).size = m.size + 1

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ m.contains k = false → (f (m.get? k)).isSome = true → (m.alter k f).size = m.size + 1

Tactic:
simp_to_raw using Raw₀.size_alter_eq_add_one

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem rfindOpt_mono {α} {f : ℕ → Option α} (H : ∀ {a m n}, m ≤ n → a ∈ f m → a ∈ f n) {a} :
    a ∈ rfindOpt f ↔ ∃ n, a ∈ f n :=
  ⟨rfindOpt_spec, fun ⟨n, h⟩ => by
    have h' := rfindOpt_dom.2 ⟨_, _, h⟩
    obtain ⟨k, hk⟩ := rfindOpt_spec ⟨h', rfl⟩
    have := (H (le_max_left _ _) h).symm.trans (H (le_max_right _ _) hk)
    simp at this; simp [this, get_mem]⟩

Proof state:
case intro
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
this : a = (rfindOpt f).get h'
⊢ a ∈ rfindOpt f

Tactic:
simp [this, get_mem]

Result:
no goals

Proof state:
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
⊢ a ∈ rfindOpt f

Tactic:
have h' := rfindOpt_dom.2 ⟨_, _, h⟩

Result:
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
⊢ a ∈ rfindOpt f

Proof state:
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
⊢ a ∈ rfindOpt f

Tactic:
obtain ⟨k, hk⟩ := rfindOpt_spec ⟨h', rfl⟩

Result:
case intro
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
⊢ a ∈ rfindOpt f

Proof state:
case intro
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
⊢ a ∈ rfindOpt f

Tactic:
have := (H (le_max_left _ _) h).symm.trans (H (le_max_right _ _) hk)

Result:
case intro
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
this : Option.some a = Option.some ((rfindOpt f).get h')
⊢ a ∈ rfindOpt f

Proof state:
case intro
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
this : Option.some a = Option.some ((rfindOpt f).get h')
⊢ a ∈ rfindOpt f

Tactic:
simp at this

Result:
case intro
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
this : a = (rfindOpt f).get h'
⊢ a ∈ rfindOpt f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem decide_eq_false {p : Prop} {_ : Decidable p} : p = False → decide p = false

Proof state:
p : Prop
x✝ : Decidable p
⊢ p = False → decide p = false

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
@[simp]
lemma finsuppLeft_symm_apply_single (i : ι) (m : M) (n : N) :
    (finsuppLeft R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) =
      Finsupp.single i m ⊗ₜ[R] n

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
i : ι
m : M
n : N
⊢ (finsuppLeft R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) = Finsupp.single i m ⊗ₜ[R] n

Tactic:
simp [finsuppLeft, Finsupp.lsum]

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem map_comp_reindex_symm (f : Π i, s i →ₗ[R] t i) (e : ι ≃ ι₂) :
    map f ∘ₗ (reindex R s e).symm = (reindex R t e).symm ∘ₗ map (fun i => f (e.symm i))

Proof state:
case H.H
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
e : ι ≃ ι₂
m : (i : ι₂) → s (e.symm i)
⊢ ((map f ∘ₗ ↑(reindex R s e).symm).compMultilinearMap (tprod R)) m =
    ((↑(reindex R t e).symm ∘ₗ map fun i => f (e.symm i)).compMultilinearMap (tprod R)) m

Tactic:
apply LinearEquiv.injective (reindex R t e)

Result:
case H.H.a
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
e : ι ≃ ι₂
m : (i : ι₂) → s (e.symm i)
⊢ (reindex R t e) (((map f ∘ₗ ↑(reindex R s e).symm).compMultilinearMap (tprod R)) m) =
    (reindex R t e) (((↑(reindex R t e).symm ∘ₗ map fun i => f (e.symm i)).compMultilinearMap (tprod R)) m)

Proof state:
case H.H.a
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
e : ι ≃ ι₂
m : (i : ι₂) → s (e.symm i)
⊢ (reindex R t e) (((map f ∘ₗ ↑(reindex R s e).symm).compMultilinearMap (tprod R)) m) =
    (reindex R t e) (((↑(reindex R t e).symm ∘ₗ map fun i => f (e.symm i)).compMultilinearMap (tprod R)) m)

Tactic:
simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, LinearEquiv.coe_coe,
  comp_apply, ← map_reindex, LinearEquiv.apply_symm_apply, map_tprod]

Result:
no goals

Proof state:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
e : ι ≃ ι₂
⊢ map f ∘ₗ ↑(reindex R s e).symm = ↑(reindex R t e).symm ∘ₗ map fun i => f (e.symm i)

Tactic:
ext m

Result:
case H.H
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
e : ι ≃ ι₂
m : (i : ι₂) → s (e.symm i)
⊢ ((map f ∘ₗ ↑(reindex R s e).symm).compMultilinearMap (tprod R)) m =
    ((↑(reindex R t e).symm ∘ₗ map fun i => f (e.symm i)).compMultilinearMap (tprod R)) m
-- Mathlib/Topology/Order.lean
theorem nhds_mkOfNhds_single [DecidableEq α] {a₀ : α} {l : Filter α} (h : pure a₀ ≤ l) (b : α) :
    @nhds α (TopologicalSpace.mkOfNhds (update pure a₀ l)) b =
      (update pure a₀ l : α → Filter α) b

Proof state:
case inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
⊢ ∀ᶠ (y : α) in update pure a l a, s ∈ update pure a l y

Tactic:
filter_upwards [hs] with b hb

Result:
case h
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
b : α
hb : b ∈ s
⊢ s ∈ update pure a l b

Proof state:
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
⊢ ∀ᶠ (y : α) in update pure a₀ l a, s ∈ update pure a₀ l y

Tactic:
rcases eq_or_ne a a₀ with (rfl | ha)

Result:
case inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
⊢ ∀ᶠ (y : α) in update pure a l a, s ∈ update pure a l y

case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
ha : a ≠ a₀
⊢ ∀ᶠ (y : α) in update pure a₀ l a, s ∈ update pure a₀ l y

Proof state:
case h
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
b : α
hb : b ∈ s
⊢ s ∈ update pure a l b

Tactic:
rcases eq_or_ne b a with (rfl | hb)

Result:
case h.inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ : α
s : Set α
b : α
hb : b ∈ s
h : pure b ≤ l
hs : s ∈ update pure b l b
⊢ s ∈ update pure b l b

case h.inr
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
b : α
hb✝ : b ∈ s
hb : b ≠ a
⊢ s ∈ update pure a l b

Proof state:
case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
ha : a ≠ a₀
⊢ ∀ᶠ (y : α) in update pure a₀ l a, s ∈ update pure a₀ l y

Tactic:
simpa only [update_of_ne ha, mem_pure, eventually_pure] using hs

Result:
no goals

Proof state:
case h.inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ : α
s : Set α
b : α
hb : b ∈ s
h : pure b ≤ l
hs : s ∈ update pure b l b
⊢ s ∈ update pure b l b

Tactic:
exact hs

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b : α
⊢ 𝓝 b = update pure a₀ l b

Tactic:
refine nhds_mkOfNhds _ _ (le_update_iff.mpr ⟨h, fun _ _ => le_rfl⟩) fun a s hs => ?_

Result:
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
⊢ ∀ᶠ (y : α) in update pure a₀ l a, s ∈ update pure a₀ l y

Proof state:
case h.inr
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
b : α
hb✝ : b ∈ s
hb : b ≠ a
⊢ s ∈ update pure a l b

Tactic:
rwa [update_of_ne hb]

Result:
no goals