harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/FinRange.lean
theorem finRange_reverse (n) : (finRange n).reverse = (finRange n).map Fin.rev

Proof state:
case succ
n : Nat
ih : (finRange n).reverse = map Fin.rev (finRange n)
⊢ (map Fin.castSucc (finRange n) ++ [Fin.last n]).reverse = map Fin.rev (finRange (n + 1))

Tactic:
conv => rhs; rw [finRange_succ]

Result:
case succ
n : Nat
ih : (finRange n).reverse = map Fin.rev (finRange n)
⊢ (map Fin.castSucc (finRange n) ++ [Fin.last n]).reverse = map Fin.rev (0 :: map Fin.succ (finRange n))

Proof state:
case succ.e_tail.e_f
n : Nat
ih : (finRange n).reverse = map Fin.rev (finRange n)
⊢ Fin.castSucc ∘ Fin.rev = Fin.rev ∘ Fin.succ

Tactic:
funext

Result:
case succ.e_tail.e_f.h
n : Nat
ih : (finRange n).reverse = map Fin.rev (finRange n)
x✝ : Fin n
⊢ (Fin.castSucc ∘ Fin.rev) x✝ = (Fin.rev ∘ Fin.succ) x✝

Proof state:
n : Nat
⊢ (finRange n).reverse = map Fin.rev (finRange n)

Tactic:
induction n with
| zero => simp
| succ n ih =>
  conv => lhs; rw [finRange_succ_last]
  conv => rhs; rw [finRange_succ]
  rw [reverse_append, reverse_cons, reverse_nil, nil_append, singleton_append, ← map_reverse,
    map_cons, ih, map_map, map_map]
  congr; funext
  simp [Fin.rev_succ]

Result:
no goals

Proof state:
case zero

⊢ (finRange 0).reverse = map Fin.rev (finRange 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ
n : Nat
ih : (finRange n).reverse = map Fin.rev (finRange n)
⊢ (finRange (n + 1)).reverse = map Fin.rev (finRange (n + 1))

Tactic:
conv => lhs; rw [finRange_succ_last]

Result:
case succ
n : Nat
ih : (finRange n).reverse = map Fin.rev (finRange n)
⊢ (map Fin.castSucc (finRange n) ++ [Fin.last n]).reverse = map Fin.rev (finRange (n + 1))

Proof state:
case succ
n : Nat
ih : (finRange n).reverse = map Fin.rev (finRange n)
⊢ Fin.last n :: map (Fin.castSucc ∘ Fin.rev) (finRange n) = Fin.rev 0 :: map (Fin.rev ∘ Fin.succ) (finRange n)

Tactic:
congr

Result:
case succ.e_tail.e_f
n : Nat
ih : (finRange n).reverse = map Fin.rev (finRange n)
⊢ Fin.castSucc ∘ Fin.rev = Fin.rev ∘ Fin.succ

Proof state:
case succ
n : Nat
ih : (finRange n).reverse = map Fin.rev (finRange n)
⊢ (map Fin.castSucc (finRange n) ++ [Fin.last n]).reverse = map Fin.rev (0 :: map Fin.succ (finRange n))

Tactic:
rw [reverse_append, reverse_cons, reverse_nil, nil_append, singleton_append, ← map_reverse,
  map_cons, ih, map_map, map_map]

Result:
case succ
n : Nat
ih : (finRange n).reverse = map Fin.rev (finRange n)
⊢ Fin.last n :: map (Fin.castSucc ∘ Fin.rev) (finRange n) = Fin.rev 0 :: map (Fin.rev ∘ Fin.succ) (finRange n)

Proof state:
case succ.e_tail.e_f.h
n : Nat
ih : (finRange n).reverse = map Fin.rev (finRange n)
x✝ : Fin n
⊢ (Fin.castSucc ∘ Fin.rev) x✝ = (Fin.rev ∘ Fin.succ) x✝

Tactic:
simp [Fin.rev_succ]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/FloorPow.lean
theorem tendsto_div_of_monotone_of_tendsto_div_floor_pow (u : ℕ → ℝ) (l : ℝ) (hmono : Monotone u)
    (c : ℕ → ℝ) (cone : ∀ k, 1 < c k) (clim : Tendsto c atTop (𝓝 1))
    (hc : ∀ k, Tendsto (fun n : ℕ => u ⌊c k ^ n⌋₊ / ⌊c k ^ n⌋₊) atTop (𝓝 l)) :
    Tendsto (fun n => u n / n) atTop (𝓝 l)

Proof state:
case refine_1
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n => c k ^ (n + 1)) atTop atTop

Tactic:
exact (tendsto_pow_atTop_atTop_of_one_lt (cone k)).comp (tendsto_add_atTop_nat 1)

Result:
no goals

Proof state:
case refine_1
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1)) atTop (𝓝 1)

Tactic:
refine tendsto_nat_floor_div_atTop.comp ?_

Result:
case refine_1
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n => c k ^ (n + 1)) atTop atTop
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleOf_eq_one_iff (f : Perm α) [DecidableRel f.SameCycle] : cycleOf f x = 1 ↔ f x = x

Proof state:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
⊢ (∀ (x_1 : α), (if f.SameCycle x x_1 then f x_1 else x_1) = x_1) ↔ f x = x

Tactic:
refine ⟨fun h => (if_pos (SameCycle.refl f x)).symm.trans (h x), fun h y => ?_⟩

Result:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
h : f x = x
y : α
⊢ (if f.SameCycle x y then f y else y) = y

Proof state:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
h : f x = x
y : α
hy : ¬f y = y
⊢ ¬(f x = x ↔ f y = y)

Tactic:
tauto

Result:
no goals

Proof state:
case pos
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
h : f x = x
y : α
hy : f y = y
⊢ (if f.SameCycle x y then f y else y) = y

Tactic:
rw [hy, ite_self]

Result:
no goals

Proof state:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
⊢ f.cycleOf x = 1 ↔ f x = x

Tactic:
simp_rw [Perm.ext_iff, cycleOf_apply, one_apply]

Result:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
⊢ (∀ (x_1 : α), (if f.SameCycle x x_1 then f x_1 else x_1) = x_1) ↔ f x = x

Proof state:
case neg
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
h : f x = x
y : α
hy : ¬f y = y
⊢ (if f.SameCycle x y then f y else y) = y

Tactic:
exact if_neg (mt SameCycle.apply_eq_self_iff (by tauto))

Result:
no goals

Proof state:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
h : f x = x
y : α
⊢ (if f.SameCycle x y then f y else y) = y

Tactic:
by_cases hy : f y = y

Result:
case pos
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
h : f x = x
y : α
hy : f y = y
⊢ (if f.SameCycle x y then f y else y) = y

case neg
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
h : f x = x
y : α
hy : ¬f y = y
⊢ (if f.SameCycle x y then f y else y) = y
-- Mathlib/Algebra/MonoidAlgebra/Basic.lean
@[simp]
lemma mapDomainAlgHom_id (k A) [CommSemiring k] [Semiring A] [Algebra k A] :
    mapDomainAlgHom k A (MonoidHom.id G) = AlgHom.id k (MonoidAlgebra A G)

Proof state:
G : Type u₂
inst✝³ : Monoid G
k : Type u_4
A : Type u_5
inst✝² : CommSemiring k
inst✝¹ : Semiring A
inst✝ : Algebra k A
⊢ mapDomainAlgHom k A (MonoidHom.id G) = AlgHom.id k (MonoidAlgebra A G)

Tactic:
ext

Result:
case H.H
G : Type u₂
inst✝³ : Monoid G
k : Type u_4
A : Type u_5
inst✝² : CommSemiring k
inst✝¹ : Semiring A
inst✝ : Algebra k A
x✝¹ : MonoidAlgebra A G
x✝ : G
⊢ ((mapDomainAlgHom k A (MonoidHom.id G)) x✝¹) x✝ = ((AlgHom.id k (MonoidAlgebra A G)) x✝¹) x✝

Proof state:
case H.H
G : Type u₂
inst✝³ : Monoid G
k : Type u_4
A : Type u_5
inst✝² : CommSemiring k
inst✝¹ : Semiring A
inst✝ : Algebra k A
x✝¹ : MonoidAlgebra A G
x✝ : G
⊢ ((mapDomainAlgHom k A (MonoidHom.id G)) x✝¹) x✝ = ((AlgHom.id k (MonoidAlgebra A G)) x✝¹) x✝

Tactic:
simp [MonoidHom.id, ← Function.id_def]

Result:
no goals
-- Mathlib/Data/List/Forall2.lean
theorem forall₂_reverse_iff {l₁ l₂} : Forall₂ R (reverse l₁) (reverse l₂) ↔ Forall₂ R l₁ l₂ :=
  Iff.intro
    (fun h => by
      rw [← reverse_reverse l₁, ← reverse_reverse l₂]
      exact rel_reverse h)
    fun h => rel_reverse h

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
⊢ Forall₂ R l₁.reverse.reverse l₂.reverse.reverse

Tactic:
exact rel_reverse h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
⊢ Forall₂ R l₁ l₂

Tactic:
rw [← reverse_reverse l₁, ← reverse_reverse l₂]

Result:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
⊢ Forall₂ R l₁.reverse.reverse l₂.reverse.reverse
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le.intro {a b : Int} (n : Nat) (h : a + n = b) : a ≤ b :=
  le.intro_sub n <| by rw [← h, Int.add_comm]; simp [Int.sub_eq_add_neg, Int.add_assoc]

Proof state:
a b : Int
n : Nat
h : a + ↑n = b
⊢ ↑n + a - a = ↑n

Tactic:
simp [Int.sub_eq_add_neg, Int.add_assoc]

Result:
no goals

Proof state:
a b : Int
n : Nat
h : a + ↑n = b
⊢ b - a = ↑n

Tactic:
rw [← h, Int.add_comm]

Result:
a b : Int
n : Nat
h : a + ↑n = b
⊢ ↑n + a - a = ↑n
-- Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
theorem contMDiffOn_prod_module_iff (f : M → F₁ × F₂) :
    ContMDiffOn I 𝓘(𝕜, F₁ × F₂) n f s ↔
      ContMDiffOn I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s ∧ ContMDiffOn I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffOn I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) n f s ↔
    ContMDiffOn I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s ∧ ContMDiffOn I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s

Tactic:
exact contMDiffOn_prod_iff f

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffOn I 𝓘(𝕜, F₁ × F₂) n f s ↔
    ContMDiffOn I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s ∧ ContMDiffOn I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

Result:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffOn I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) n f s ↔
    ContMDiffOn I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s ∧ ContMDiffOn I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s
-- Mathlib/Order/RelSeries.lean
@[simp]
lemma last_singleton {r : Rel α α} (x : α) : (singleton r x).last = x

Proof state:
α : Type u_1
r : Rel α α
x : α
⊢ (singleton r x).last = x

Tactic:
simp [singleton, last]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
lemma tendsto_measure_Icc [NoAtoms μ] (b : ℝ) :
    Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝 (0 : ℝ)) (𝓝 0)

Proof state:
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NoAtoms μ
b r : ℝ
hr : r < 0
⊢ ¬b - r ≤ b + r

Tactic:
linarith

Result:
no goals

Proof state:
case left
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NoAtoms μ
b : ℝ
⊢ (fun x => 0) =ᶠ[𝓝[<] 0] fun δ => μ (Icc (b - δ) (b + δ))

Tactic:
filter_upwards [self_mem_nhdsWithin] with r (hr : r < 0)

Result:
case h
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NoAtoms μ
b r : ℝ
hr : r < 0
⊢ 0 = μ (Icc (b - r) (b + r))

Proof state:
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NoAtoms μ
b : ℝ
⊢ Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝 0) (𝓝 0)

Tactic:
rw [← nhdsLT_sup_nhdsGE, tendsto_sup]

Result:
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NoAtoms μ
b : ℝ
⊢ Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0) ∧ Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 0)

Proof state:
case h
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NoAtoms μ
b r : ℝ
hr : r < 0
⊢ 0 = μ (Icc (b - r) (b + r))

Tactic:
rw [Icc_eq_empty (by linarith), measure_empty]

Result:
no goals

Proof state:
case left
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NoAtoms μ
b : ℝ
⊢ Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0)

Tactic:
apply tendsto_const_nhds.congr'

Result:
case left
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NoAtoms μ
b : ℝ
⊢ (fun x => 0) =ᶠ[𝓝[<] 0] fun δ => μ (Icc (b - δ) (b + δ))

Proof state:
case right
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NoAtoms μ
b : ℝ
⊢ Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 0)

Tactic:
simpa only [measure_singleton] using tendsto_measure_Icc_nhdsWithin_right μ b

Result:
no goals

Proof state:
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NoAtoms μ
b : ℝ
⊢ Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0) ∧ Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 0)

Tactic:
constructor

Result:
case left
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NoAtoms μ
b : ℝ
⊢ Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0)

case right
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NoAtoms μ
b : ℝ
⊢ Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 0)
-- Mathlib/LinearAlgebra/Dimension/Finrank.lean
theorem finrank_le_finrank_of_rank_le_rank
    (h : lift.{w} (Module.rank R M) ≤ Cardinal.lift.{v} (Module.rank R N))
    (h' : Module.rank R N < ℵ₀) : finrank R M ≤ finrank R N

Proof state:
R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} (Module.rank R N)
h' : Module.rank R N < ℵ₀
⊢ finrank R M ≤ finrank R N

Tactic:
simpa only [toNat_lift] using toNat_le_toNat h (lift_lt_aleph0.mpr h')

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem divides_sq_eq_zero_z {x y : ℤ} (h : x * x = d * y * y) : x = 0 ∧ y = 0

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : ↑(x.natAbs * x.natAbs) = ↑(d * y.natAbs * y.natAbs)
⊢ x = 0 ∧ y = 0

Tactic:
exact
  let ⟨h1, h2⟩ := divides_sq_eq_zero (Int.ofNat.inj h)
  ⟨Int.natAbs_eq_zero.mp h1, Int.natAbs_eq_zero.mp h2⟩

Result:
no goals

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : x * x = ↑d * y * y
⊢ x = 0 ∧ y = 0

Tactic:
rw [mul_assoc, ← Int.natAbs_mul_self, ← Int.natAbs_mul_self, ← Int.ofNat_mul, ← mul_assoc] at h

Result:
d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : ↑(x.natAbs * x.natAbs) = ↑(d * y.natAbs * y.natAbs)
⊢ x = 0 ∧ y = 0
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_eq_zero' {m : M} (s : S) : mk' f m s = 0 ↔ ∃ s' : S, s' • m = 0

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ mk' f m s = 0 ↔ ∃ s', s' • m = 0

Tactic:
simp_rw [← mk'_zero f (1 : S), mk'_eq_mk'_iff, smul_zero, one_smul, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem forall_mem_filter {l : List α} {p : α → Bool} {P : α → Prop} :
    (∀ (i) (_ : i ∈ l.filter p), P i) ↔ ∀ (j) (_ : j ∈ l), p j → P j

Proof state:
α : Type u_1
l : List α
p : α → Bool
P : α → Prop
⊢ (∀ (i : α), i ∈ filter p l → P i) ↔ ∀ (j : α), j ∈ l → p j = true → P j

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem forall_zero_iff {P : Vector α 0 → Prop} :
    (∀ v, P v) ↔ P #v[]

Proof state:
case mp
α : Type u_1
P : Vector α 0 → Prop
h : ∀ (v : Vector α 0), P v
⊢ P { toArray := #[], size_toArray := ⋯ }

Tactic:
apply h

Result:
no goals

Proof state:
α : Type u_1
P : Vector α 0 → Prop
⊢ (∀ (v : Vector α 0), P v) ↔ P { toArray := #[], size_toArray := ⋯ }

Tactic:
constructor

Result:
case mp
α : Type u_1
P : Vector α 0 → Prop
⊢ (∀ (v : Vector α 0), P v) → P { toArray := #[], size_toArray := ⋯ }

case mpr
α : Type u_1
P : Vector α 0 → Prop
⊢ P { toArray := #[], size_toArray := ⋯ } → ∀ (v : Vector α 0), P v

Proof state:
case mp
α : Type u_1
P : Vector α 0 → Prop
⊢ (∀ (v : Vector α 0), P v) → P { toArray := #[], size_toArray := ⋯ }

Tactic:
intro h

Result:
case mp
α : Type u_1
P : Vector α 0 → Prop
h : ∀ (v : Vector α 0), P v
⊢ P { toArray := #[], size_toArray := ⋯ }

Proof state:
case mpr
α : Type u_1
P : Vector α 0 → Prop
h : P { toArray := #[], size_toArray := ⋯ }
v : Vector α 0
⊢ P v

Tactic:
obtain (rfl : v = #v[]) := (by ext i h; simp at h)

Result:
case mpr
α : Type u_1
P : Vector α 0 → Prop
h : P { toArray := #[], size_toArray := ⋯ }
⊢ P { toArray := #[], size_toArray := ⋯ }

Proof state:
α : Type u_1
P : Vector α 0 → Prop
h : P { toArray := #[], size_toArray := ⋯ }
v : Vector α 0
⊢ v = { toArray := #[], size_toArray := ⋯ }

Tactic:
ext i h

Result:
case h
α : Type u_1
P : Vector α 0 → Prop
h✝ : P { toArray := #[], size_toArray := ⋯ }
v : Vector α 0
i : Nat
h : i < 0
⊢ v[i] = { toArray := #[], size_toArray := ⋯ }[i]

Proof state:
case mpr
α : Type u_1
P : Vector α 0 → Prop
⊢ P { toArray := #[], size_toArray := ⋯ } → ∀ (v : Vector α 0), P v

Tactic:
intro h v

Result:
case mpr
α : Type u_1
P : Vector α 0 → Prop
h : P { toArray := #[], size_toArray := ⋯ }
v : Vector α 0
⊢ P v

Proof state:
case mpr
α : Type u_1
P : Vector α 0 → Prop
h : P { toArray := #[], size_toArray := ⋯ }
⊢ P { toArray := #[], size_toArray := ⋯ }

Tactic:
apply h

Result:
no goals

Proof state:
case h
α : Type u_1
P : Vector α 0 → Prop
h✝ : P { toArray := #[], size_toArray := ⋯ }
v : Vector α 0
i : Nat
h : i < 0
⊢ v[i] = { toArray := #[], size_toArray := ⋯ }[i]

Tactic:
simp at h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem dropWhile_append_of_pos {p : α → Bool} {l₁ l₂ : List α} (h : ∀ a ∈ l₁, p a) :
    (l₁ ++ l₂).dropWhile p = l₂.dropWhile p

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : ∀ (a : α), a ∈ l₁ → p a = true
⊢ dropWhile p (l₁ ++ l₂) = dropWhile p l₂

Tactic:
induction l₁ with
| nil => simp
| cons x xs ih => simp_all [dropWhile_cons]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
l₂ : List α
h : ∀ (a : α), a ∈ [] → p a = true
⊢ dropWhile p ([] ++ l₂) = dropWhile p l₂

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
l₂ : List α
x : α
xs : List α
ih : (∀ (a : α), a ∈ xs → p a = true) → dropWhile p (xs ++ l₂) = dropWhile p l₂
h : ∀ (a : α), a ∈ x :: xs → p a = true
⊢ dropWhile p (x :: xs ++ l₂) = dropWhile p l₂

Tactic:
simp_all [dropWhile_cons]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Divisibility.lean
theorem is_prime_iff {a : Cardinal} : Prime a ↔ ℵ₀ ≤ a ∨ ∃ p : ℕ, a = p ∧ p.Prime

Proof state:
a : Cardinal.{u_1}
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p

Tactic:
rcases le_or_lt ℵ₀ a with h | h

Result:
case inl
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p

case inr
a : Cardinal.{u_1}
h : a < ℵ₀
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p

Proof state:
case inr.intro
a : ℕ
h : ↑a < ℵ₀
⊢ Prime ↑a ↔ ℵ₀ ≤ ↑a ∨ ∃ p, ↑a = ↑p ∧ Nat.Prime p

Tactic:
simp [not_le.mpr h]

Result:
no goals

Proof state:
case inl
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p

Tactic:
simp [h]

Result:
no goals

Proof state:
case inr
a : Cardinal.{u_1}
h : a < ℵ₀
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p

Tactic:
lift a to ℕ using id h

Result:
case inr.intro
a : ℕ
h : ↑a < ℵ₀
⊢ Prime ↑a ↔ ℵ₀ ≤ ↑a ∨ ∃ p, ↑a = ↑p ∧ Nat.Prime p
-- Mathlib/Topology/Basic.lean
theorem Set.Finite.isClosed_biUnion {s : Set α} {f : α → Set X} (hs : s.Finite)
    (h : ∀ i ∈ s, IsClosed (f i)) :
    IsClosed (⋃ i ∈ s, f i)

Proof state:
X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
s : Set α
f : α → Set X
hs : s.Finite
h : ∀ i ∈ s, IsOpen (f i)ᶜ
⊢ IsOpen (⋂ i ∈ s, (f i)ᶜ)

Tactic:
exact hs.isOpen_biInter h

Result:
no goals

Proof state:
X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
s : Set α
f : α → Set X
hs : s.Finite
h : ∀ i ∈ s, IsClosed (f i)
⊢ IsClosed (⋃ i ∈ s, f i)

Tactic:
simp only [← isOpen_compl_iff, compl_iUnion] at *

Result:
X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
s : Set α
f : α → Set X
hs : s.Finite
h : ∀ i ∈ s, IsOpen (f i)ᶜ
⊢ IsOpen (⋂ i ∈ s, (f i)ᶜ)
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_eq_zero_iff {v : E} : orthogonalProjection K v = 0 ↔ v ∈ Kᗮ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
⊢ (orthogonalProjection K) v = 0 ↔ v ∈ Kᗮ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Subtype.eq <| eq_orthogonalProjection_of_mem_orthogonal
  (zero_mem _) ?_⟩

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
h : (orthogonalProjection K) v = 0
⊢ v ∈ Kᗮ

case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
h : v ∈ Kᗮ
⊢ v - ↑0 ∈ Kᗮ

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
h : (orthogonalProjection K) v = 0
⊢ v ∈ Kᗮ

Tactic:
simpa [h] using sub_orthogonalProjection_mem_orthogonal (K := K) v

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
h : v ∈ Kᗮ
⊢ v - ↑0 ∈ Kᗮ

Tactic:
simpa

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/PureCoherence.lean
theorem naturality_inv {p : a ⟶ b} {f g : b ⟶ c} {pf : a ⟶ c}
    {η : f ≅ g} (η_f : p ≫ f ≅ pf) (η_g : p ≫ g ≅ pf) (ih : p ◁ η ≪≫ η_g = η_f) :
    p ◁ η.symm ≪≫ η_f = η_g

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f g : b ⟶ c
pf : a ⟶ c
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g = η_g

Tactic:
apply Iso.ext (by simp)

Result:
no goals

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f g : b ⟶ c
pf : a ⟶ c
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η.symm ≪≫ η_f = η_g

Tactic:
rw [← ih]

Result:
B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f g : b ⟶ c
pf : a ⟶ c
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g = η_g

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f g : b ⟶ c
pf : a ⟶ c
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g).hom = η_g.hom

Tactic:
simp

Result:
no goals