harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/List.lean
theorem tendsto_nhds {β : Type*} {f : List α → β} {r : List α → Filter β}
    (h_nil : Tendsto f (pure []) (r []))
    (h_cons :
      ∀ l a,
        Tendsto f (𝓝 l) (r l) →
          Tendsto (fun p : α × List α => f (p.1::p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a::l))) :
    ∀ l, Tendsto f (𝓝 l) (r l)
  | [] => by rwa [nhds_nil]
  | a::l => by
    rw [tendsto_cons_iff]; exact h_cons l a (@tendsto_nhds _ _ _ h_nil h_cons l)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
⊢ Tendsto f (𝓝 []) (r [])

Tactic:
rwa [nhds_nil]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
a : α
l : List α
⊢ Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))

Tactic:
exact h_cons l a (@tendsto_nhds _ _ _ h_nil h_cons l)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
a : α
l : List α
⊢ Tendsto f (𝓝 (a :: l)) (r (a :: l))

Tactic:
rw [tendsto_cons_iff]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
a : α
l : List α
⊢ Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_insertEntry [BEq α] [EquivBEq α] [Inhabited α]  {l : List ((a : α) × β a)}
    {k a : α} {v : β k} : getKey! a (insertEntry k v l) =
      if k == a then k else getKey! a l

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ getKey! a (insertEntry k v l) = if (k == a) = true then k else getKey! a l

Tactic:
simp [getKey!_eq_getKey?, getKey?_insertEntry, apply_ite Option.get!]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem sup_neBot {f g : Filter α} : NeBot (f ⊔ g) ↔ NeBot f ∨ NeBot g

Proof state:
α : Type u
f g : Filter α
⊢ (f ⊔ g).NeBot ↔ f.NeBot ∨ g.NeBot

Tactic:
simp only [neBot_iff, not_and_or, Ne, sup_eq_bot_iff]

Result:
no goals
-- Mathlib/Data/PNat/Prime.lean
theorem Coprime.factor_eq_gcd_left_right {a b m n : ℕ+} (cop : m.Coprime n) (am : a ∣ m)
    (bn : b ∣ n) : a = m.gcd (a * b)

Proof state:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (a * b).gcd m

Tactic:
apply Coprime.factor_eq_gcd_left cop am bn

Result:
no goals

Proof state:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = m.gcd (a * b)

Tactic:
rw [gcd_comm]

Result:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (a * b).gcd m
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem _root_.QuotientAddGroup.norm_lift_apply_le {S : AddSubgroup M} (f : NormedAddGroupHom M N)
    (hf : ∀ x ∈ S, f x = 0) (x : M ⧸ S) : ‖lift S f.toAddMonoidHom hf x‖ ≤ ‖f‖ * ‖x‖

Proof state:
case inr.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
h : 0 < ‖f‖
x : M
hx : ‖x‖ < ‖(lift S f.toAddMonoidHom hf) ↑x‖ / ‖f‖
⊢ False

Tactic:
exact ((lt_div_iff₀' h).1 hx).not_le (le_opNorm f x)

Result:
no goals

Proof state:
case inl
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
h : ‖f‖ = 0
⊢ ‖(lift S f.toAddMonoidHom hf) x‖ ≤ ‖f‖ * ‖x‖

Tactic:
rcases mk_surjective x with ⟨x, rfl⟩

Result:
case inl.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
h : ‖f‖ = 0
x : M
⊢ ‖(lift S f.toAddMonoidHom hf) ↑x‖ ≤ ‖f‖ * ‖↑x‖

Proof state:
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ‖(lift S f.toAddMonoidHom hf) x‖ ≤ ‖f‖ * ‖x‖

Tactic:
rw [← not_lt, ← lt_div_iff₀' h, norm_lt_iff]

Result:
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ¬∃ m, ↑m = x ∧ ‖m‖ < ‖(lift S f.toAddMonoidHom hf) x‖ / ‖f‖

Proof state:
case inl.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
h : ‖f‖ = 0
x : M
⊢ ‖(lift S f.toAddMonoidHom hf) ↑x‖ ≤ ‖f‖ * ‖↑x‖

Tactic:
simpa [h] using le_opNorm f x

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
⊢ ‖(lift S f.toAddMonoidHom hf) x‖ ≤ ‖f‖ * ‖x‖

Tactic:
cases (norm_nonneg f).eq_or_gt with
| inl h =>
  rcases mk_surjective x with ⟨x, rfl⟩
  simpa [h] using le_opNorm f x
| inr h =>
  rw [← not_lt, ← lt_div_iff₀' h, norm_lt_iff]
  rintro ⟨x, rfl, hx⟩
  exact ((lt_div_iff₀' h).1 hx).not_le (le_opNorm f x)

Result:
no goals

Proof state:
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ¬∃ m, ↑m = x ∧ ‖m‖ < ‖(lift S f.toAddMonoidHom hf) x‖ / ‖f‖

Tactic:
rintro ⟨x, rfl, hx⟩

Result:
case inr.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
h : 0 < ‖f‖
x : M
hx : ‖x‖ < ‖(lift S f.toAddMonoidHom hf) ↑x‖ / ‖f‖
⊢ False
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem superpolynomialDecay_const_mul_iff [ContinuousMul β] {c : β} (hc0 : c ≠ 0) :
    (SuperpolynomialDecay l k fun n => c * f n) ↔ SuperpolynomialDecay l k f :=
  ⟨fun h => (h.const_mul c⁻¹).congr fun x => by simp [← mul_assoc, inv_mul_cancel₀ hc0], fun h =>
    h.const_mul c⟩

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Field β
inst✝ : ContinuousMul β
c : β
hc0 : c ≠ 0
h : SuperpolynomialDecay l k fun n => c * f n
x : α
⊢ c⁻¹ * (c * f x) = f x

Tactic:
simp [← mul_assoc, inv_mul_cancel₀ hc0]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullbackWithin_add_apply :
    mpullbackWithin I I' f (V + V₁) s x =
      mpullbackWithin I I' f V s x + mpullbackWithin I I' f V₁ s x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
V V₁ : (x : M') → TangentSpace I' x
⊢ mpullbackWithin I I' f (V + V₁) s x = mpullbackWithin I I' f V s x + mpullbackWithin I I' f V₁ s x

Tactic:
simp [mpullbackWithin_apply]

Result:
no goals
-- Mathlib/Algebra/Star/Conjneg.lean
@[simp] lemma conjneg_mul (f g : G → R) : conjneg (f * g) = conjneg f * conjneg g

Proof state:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f g : G → R
x✝ : G
⊢ conjneg (f * g) x✝ = (conjneg f * conjneg g) x✝

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f g : G → R
⊢ conjneg (f * g) = conjneg f * conjneg g

Tactic:
ext

Result:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f g : G → R
x✝ : G
⊢ conjneg (f * g) x✝ = (conjneg f * conjneg g) x✝
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem thickening_closure : thickening δ (closure s) = thickening δ s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
⊢ thickening δ (closure s) = thickening δ s

Tactic:
simp_rw [thickening, infEdist_closure]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearPMap.lean
theorem IsClosable.existsUnique {f : E →ₗ.[R] F} (hf : f.IsClosable) :
    ∃! f' : E →ₗ.[R] F, f.graph.topologicalClosure = f'.graph

Proof state:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ ∃! f', f.graph.topologicalClosure = f'.graph

Tactic:
refine existsUnique_of_exists_of_unique hf fun _ _ hy₁ hy₂ => eq_of_eq_graph ?_

Result:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
x✝¹ x✝ : E →ₗ.[R] F
hy₁ : f.graph.topologicalClosure = x✝¹.graph
hy₂ : f.graph.topologicalClosure = x✝.graph
⊢ x✝¹.graph = x✝.graph

Proof state:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
x✝¹ x✝ : E →ₗ.[R] F
hy₁ : f.graph.topologicalClosure = x✝¹.graph
hy₂ : f.graph.topologicalClosure = x✝.graph
⊢ x✝¹.graph = x✝.graph

Tactic:
rw [← hy₁, ← hy₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_pos_iff_exists_push {xs : Array α} :
    0 < xs.size ↔ ∃ (ys : Array α) (a : α), xs = ys.push a :=
  ⟨exists_push_of_size_pos, fun ⟨_, _, eq⟩ => by simp [eq]⟩

Proof state:
α : Type u_1
xs : Array α
x✝ : ∃ ys a, xs = ys.push a
w✝¹ : Array α
w✝ : α
eq : xs = w✝¹.push w✝
⊢ 0 < xs.size

Tactic:
simp [eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatMap_append (xs ys : Vector α n) (f : α → Vector β m) :
    (xs ++ ys).flatMap f = (xs.flatMap f ++ ys.flatMap f).cast (by simp [Nat.add_mul])

Proof state:
α : Type ?u.328929
n : Nat
β : Type ?u.328937
m : Nat
xs ys : Vector α n
f : α → Vector β m
⊢ n * m + n * m = (n + n) * m

Tactic:
simp [Nat.add_mul]

Result:
no goals

Proof state:
case mk
α : Type u_1
n : Nat
β : Type u_2
m : Nat
ys : Vector α n
f : α → Vector β m
xs : Array α
size_toArray✝ : xs.size = n
⊢ ({ toArray := xs, size_toArray := size_toArray✝ } ++ ys).flatMap f =
    Vector.cast ⋯ ({ toArray := xs, size_toArray := size_toArray✝ }.flatMap f ++ ys.flatMap f)

Tactic:
rcases ys with ⟨ys⟩

Result:
case mk.mk
α : Type u_1
n : Nat
β : Type u_2
m : Nat
f : α → Vector β m
xs : Array α
size_toArray✝¹ : xs.size = n
ys : Array α
size_toArray✝ : ys.size = n
⊢ ({ toArray := xs, size_toArray := size_toArray✝¹ } ++ { toArray := ys, size_toArray := size_toArray✝ }).flatMap f =
    Vector.cast ⋯
      ({ toArray := xs, size_toArray := size_toArray✝¹ }.flatMap f ++
        { toArray := ys, size_toArray := size_toArray✝ }.flatMap f)

Proof state:
α : Type u_1
n : Nat
β : Type u_2
m : Nat
xs ys : Vector α n
f : α → Vector β m
⊢ (xs ++ ys).flatMap f = Vector.cast ⋯ (xs.flatMap f ++ ys.flatMap f)

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
n : Nat
β : Type u_2
m : Nat
ys : Vector α n
f : α → Vector β m
xs : Array α
size_toArray✝ : xs.size = n
⊢ ({ toArray := xs, size_toArray := size_toArray✝ } ++ ys).flatMap f =
    Vector.cast ⋯ ({ toArray := xs, size_toArray := size_toArray✝ }.flatMap f ++ ys.flatMap f)

Proof state:
case mk.mk
α : Type u_1
n : Nat
β : Type u_2
m : Nat
f : α → Vector β m
xs : Array α
size_toArray✝¹ : xs.size = n
ys : Array α
size_toArray✝ : ys.size = n
⊢ ({ toArray := xs, size_toArray := size_toArray✝¹ } ++ { toArray := ys, size_toArray := size_toArray✝ }).flatMap f =
    Vector.cast ⋯
      ({ toArray := xs, size_toArray := size_toArray✝¹ }.flatMap f ++
        { toArray := ys, size_toArray := size_toArray✝ }.flatMap f)

Tactic:
simp [flatMap_def, flatten_append]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem findMax_dual (t : Ordnode α) : findMax (dual t) = findMin t

Proof state:
α : Type u_1
t : Ordnode α
⊢ t.dual.findMax = t.findMin

Tactic:
rw [← findMin_dual, dual_dual]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem swap_mk (a : Array α) (h : a.size = n) (i j) (hi hj) :
    (Vector.mk a h).swap i j = Vector.mk (a.swap i j) (by simp [h]) :=
  rfl

Proof state:
α : Type ?u.14649
n : Nat
a : Array α
h : a.size = n
i j : Nat
hi : j < n
hj : i < n
⊢ (a.swap i j ⋯ ⋯).size = n

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_push_none {f : α → Option β} {a : α} {l : Array α}
    (h : f a = none) (w : stop = l.size + 1) :
    filterMap f (l.push a) 0 stop = filterMap f l

Proof state:
α : Type u_1
β : Type u_2
stop : Nat
f : α → Option β
a : α
l : Array α
h : f a = none
w : stop = l.size + 1
⊢ filterMap f (l.push a) 0 stop = filterMap f l

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
f : α → Option β
a : α
l : Array α
h : f a = none
⊢ filterMap f (l.push a) 0 (l.size + 1) = filterMap f l

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
a : α
h : f a = none
l : List α
⊢ filterMap f ({ toList := l }.push a) 0 ({ toList := l }.size + 1) = filterMap f { toList := l }

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
a : α
l : Array α
h : f a = none
⊢ filterMap f (l.push a) 0 (l.size + 1) = filterMap f l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
a : α
h : f a = none
l : List α
⊢ filterMap f ({ toList := l }.push a) 0 ({ toList := l }.size + 1) = filterMap f { toList := l }
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_smul_add_smul_left (x y : V) (r₁ r₂ : ℝ) :
    (o.oangle (r₁ • x + r₂ • y) y).sign = SignType.sign r₁ * (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ : ℝ
⊢ (o.oangle (r₁ • x + r₂ • y) y).sign = SignType.sign r₁ * (o.oangle x y).sign

Tactic:
simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm (r₁ • x), oangle_sign_smul_add_smul_right,
  mul_neg]

Result:
no goals
-- Mathlib/Data/Finset/SDiff.lean
theorem insert_sdiff_of_not_mem (s : Finset α) {t : Finset α} {x : α} (h : x ∉ t) :
    insert x s \ t = insert x (s \ t)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
x : α
h : x ∉ t
⊢ insert x s \ t = insert x (s \ t)

Tactic:
rw [← coe_inj, coe_insert, coe_sdiff, coe_sdiff, coe_insert]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
x : α
h : x ∉ t
⊢ insert x ↑s \ ↑t = insert x (↑s \ ↑t)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
x : α
h : x ∉ t
⊢ insert x ↑s \ ↑t = insert x (↑s \ ↑t)

Tactic:
exact Set.insert_diff_of_not_mem _ h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean
theorem ordinaryHypergeometricSeries_symm :
    ordinaryHypergeometricSeries 𝔸 a b c = ordinaryHypergeometricSeries 𝔸 b a c

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ (ofScalars 𝔸 fun n =>
      (↑n !)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) =
    ofScalars 𝔸 fun n =>
      (↑n !)⁻¹ * Polynomial.eval b (ascPochhammer 𝕂 n) * Polynomial.eval a (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹

Tactic:
simp [mul_assoc, mul_left_comm]

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ ordinaryHypergeometricSeries 𝔸 a b c = ordinaryHypergeometricSeries 𝔸 b a c

Tactic:
unfold ordinaryHypergeometricSeries ordinaryHypergeometricCoefficient

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ (ofScalars 𝔸 fun n =>
      (↑n !)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) =
    ofScalars 𝔸 fun n =>
      (↑n !)⁻¹ * Polynomial.eval b (ascPochhammer 𝕂 n) * Polynomial.eval a (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹
-- Mathlib/Order/Filter/Basic.lean
theorem not_disjoint_self_iff : ¬Disjoint f f ↔ f.NeBot

Proof state:
α : Type u
f : Filter α
⊢ ¬Disjoint f f ↔ f.NeBot

Tactic:
rw [disjoint_self, neBot_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_ite_eq_false_eq_true {p : Prop} [h : Decidable p] {b c : Bool} :
  ¬(ite p (b = false) (c = true)) ↔ (ite p (b = true) (c = false))

Proof state:
case isTrue
p✝ : Prop
b c : Bool
p : p✝
⊢ (¬if p✝ then b = false else c = true) ↔ if p✝ then b = true else c = false

Tactic:
simp [p]

Result:
no goals

Proof state:
p : Prop
h : Decidable p
b c : Bool
⊢ (¬if p then b = false else c = true) ↔ if p then b = true else c = false

Tactic:
cases h with | _ p => simp [p]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma IsBasis.mapEmbedding {X : Set α} (hIX : M.IsBasis I X) (f : α ↪ β) :
    (M.mapEmbedding f).IsBasis (f '' I) (f '' X)

Proof state:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α ↪ β
⊢ (M.mapEmbedding f).IsBasis (⇑f '' I) (⇑f '' X)

Tactic:
apply hIX.map

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
theorem image (h : QuasispectrumRestricts a f) : f '' quasispectrum S a = quasispectrum R a

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Algebra R S
a : A
f : S → R
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ f '' quasispectrum S a = quasispectrum R a

Tactic:
simp only [← h.algebraMap_image, Set.image_image, h.left_inv _, Set.image_id']

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem _root_.QuadraticMap.polarBilin_injective (h : IsUnit (2 : R)) :
    Function.Injective (polarBilin : QuadraticMap R M N → _)

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ Q₁.polarBilin.toQuadraticMap = Q₂.polarBilin.toQuadraticMap

Tactic:
exact congrArg toQuadraticMap h₁₂

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ ↑2 • Q₁ = ↑2 • Q₂

Tactic:
simp_rw [Nat.cast_smul_eq_nsmul R, ← QuadraticMap.toQuadraticMap_polarBilin]

Result:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ Q₁.polarBilin.toQuadraticMap = Q₂.polarBilin.toQuadraticMap

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ 2 = ↑2

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ 2 • Q₁ = 2 • Q₂

Tactic:
rw [show (2 : R) = (2 : ℕ) by rfl]

Result:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ ↑2 • Q₁ = ↑2 • Q₂

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ Q₁ = Q₂

Tactic:
apply h.smul_left_cancel.mp

Result:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ 2 • Q₁ = 2 • Q₂

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : IsUnit 2
⊢ Function.Injective polarBilin

Tactic:
intro Q₁ Q₂ h₁₂

Result:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ Q₁ = Q₂
-- Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean
theorem dist_birkhoffSum_apply_birkhoffSum (f : α → α) (g : α → E) (n : ℕ) (x : α) :
    dist (birkhoffSum f g n (f x)) (birkhoffSum f g n x) = dist (g (f^[n] x)) (g x)

Proof state:
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
f : α → α
g : α → E
n : ℕ
x : α
⊢ dist (birkhoffSum f g n (f x)) (birkhoffSum f g n x) = dist (g (f^[n] x)) (g x)

Tactic:
simp only [dist_eq_norm, birkhoffSum_apply_sub_birkhoffSum]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_append (L₁ L₂ : Array (Array α)) :
    flatten (L₁ ++ L₂) = flatten L₁ ++ flatten L₂

Proof state:
case of
α : Type u_1
L₂ : Array (Array α)
xss✝ : List (List α)
⊢ ((List.map List.toArray xss✝).toArray ++ L₂).flatten = (List.map List.toArray xss✝).toArray.flatten ++ L₂.flatten

Tactic:
induction L₂ using array₂_induction

Result:
case of.of
α : Type u_1
xss✝¹ xss✝ : List (List α)
⊢ ((List.map List.toArray xss✝¹).toArray ++ (List.map List.toArray xss✝).toArray).flatten =
    (List.map List.toArray xss✝¹).toArray.flatten ++ (List.map List.toArray xss✝).toArray.flatten

Proof state:
case of.of
α : Type u_1
xss✝¹ xss✝ : List (List α)
⊢ ((List.map List.toArray xss✝¹).toArray ++ (List.map List.toArray xss✝).toArray).flatten =
    (List.map List.toArray xss✝¹).toArray.flatten ++ (List.map List.toArray xss✝).toArray.flatten

Tactic:
simp [← List.map_append]

Result:
no goals

Proof state:
α : Type u_1
L₁ L₂ : Array (Array α)
⊢ (L₁ ++ L₂).flatten = L₁.flatten ++ L₂.flatten

Tactic:
induction L₁ using array₂_induction

Result:
case of
α : Type u_1
L₂ : Array (Array α)
xss✝ : List (List α)
⊢ ((List.map List.toArray xss✝).toArray ++ L₂).flatten = (List.map List.toArray xss✝).toArray.flatten ++ L₂.flatten