harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
theorem hasDerivAt_of_tendsto_locally_uniformly_on' [NeBot l] {s : Set 𝕜} (hs : IsOpen s)
    (hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s)
    (hf : ∀ᶠ n in l, DifferentiableOn 𝕜 (f n) s)
    (hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))) (hx : x ∈ s) : HasDerivAt g (g' x) x

Proof state:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
s : Set 𝕜
hs : IsOpen s
hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s
hf : ∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s
hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))
hx : x ∈ s
⊢ ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) ((deriv ∘ f) n x) x

Tactic:
filter_upwards [hf] with n h z hz using ((h z hz).differentiableAt (hs.mem_nhds hz)).hasDerivAt

Result:
no goals

Proof state:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
s : Set 𝕜
hs : IsOpen s
hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s
hf : ∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s
hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))
hx : x ∈ s
⊢ HasDerivAt g (g' x) x

Tactic:
refine hasDerivAt_of_tendstoLocallyUniformlyOn hs hf' ?_ hfg hx

Result:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
s : Set 𝕜
hs : IsOpen s
hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s
hf : ∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s
hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))
hx : x ∈ s
⊢ ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) ((deriv ∘ f) n x) x
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem add_mem_iff {a : A} {r s : R} : r + s ∈ σ a ↔ r ∈ σ (-↑ₐ s + a)

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r s : R
⊢ r + s ∈ σ a ↔ r ∈ σ (-↑ₐ s + a)

Tactic:
simp only [mem_iff, sub_neg_eq_add, ← sub_sub, map_add]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem sign_eq_sign_of_equiv [DecidableEq β] [Fintype β] (f : Perm α) (g : Perm β) (e : α ≃ β)
    (h : ∀ x, e (f x) = g (e x)) : sign f = sign g

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), e (f x) = g (e x)
⊢ ∀ (x : β), g x = ((e.symm.trans f).trans e) x

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), e (f x) = g (e x)
hg : g = (e.symm.trans f).trans e
⊢ sign f = sign g

Tactic:
rw [hg, sign_symm_trans_trans]

Result:
no goals

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), e (f x) = g (e x)
⊢ sign f = sign g

Tactic:
have hg : g = (e.symm.trans f).trans e := Equiv.ext <| by simp [h]

Result:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), e (f x) = g (e x)
hg : g = (e.symm.trans f).trans e
⊢ sign f = sign g
-- Mathlib/Data/Finmap.lean
lemma mem_lookup_iff {s : Finmap β} {a : α} {b : β a} :
    b ∈ s.lookup a ↔ Sigma.mk a b ∈ s.entries

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
a : α
b : β a
⊢ b ∈ lookup a s ↔ ⟨a, b⟩ ∈ s.entries

Tactic:
rcases s with ⟨⟨l⟩, hl⟩

Result:
case mk.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
entries✝ : Multiset (Sigma β)
l : List (Sigma β)
hl : Multiset.NodupKeys (Quot.mk (⇑(isSetoid (Sigma β))) l)
⊢ b ∈ lookup a { entries := Quot.mk (⇑(isSetoid (Sigma β))) l, nodupKeys := hl } ↔
    ⟨a, b⟩ ∈ { entries := Quot.mk (⇑(isSetoid (Sigma β))) l, nodupKeys := hl }.entries

Proof state:
case mk.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
entries✝ : Multiset (Sigma β)
l : List (Sigma β)
hl : Multiset.NodupKeys (Quot.mk (⇑(isSetoid (Sigma β))) l)
⊢ b ∈ lookup a { entries := Quot.mk (⇑(isSetoid (Sigma β))) l, nodupKeys := hl } ↔
    ⟨a, b⟩ ∈ { entries := Quot.mk (⇑(isSetoid (Sigma β))) l, nodupKeys := hl }.entries

Tactic:
exact List.mem_dlookup_iff hl

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem isTopologicalBasis_Iic_principal :
    IsTopologicalBasis (range (Iic ∘ 𝓟 : Set α → Set (Filter α))) :=
  { exists_subset_inter

Proof state:
case intro.intro
α : Type u_2
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ ∃ t₃ ∈ range (Iic ∘ 𝓟), l ∈ t₃ ∧ t₃ ⊆ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t

Tactic:
exact ⟨Iic (𝓟 s) ∩ Iic (𝓟 t), ⟨s ∩ t, by simp⟩, hl, Subset.rfl⟩

Result:
no goals

Proof state:
α : Type u_2
⊢ ∀ t₁ ∈ range (Iic ∘ 𝓟), ∀ t₂ ∈ range (Iic ∘ 𝓟), ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ range (Iic ∘ 𝓟), x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ l hl

Result:
case intro.intro
α : Type u_2
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ ∃ t₃ ∈ range (Iic ∘ 𝓟), l ∈ t₃ ∧ t₃ ⊆ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t

Proof state:
α : Type u_2
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ (Iic ∘ 𝓟) (s ∩ t) = Iic (𝓟 s) ∩ Iic (𝓟 t)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem empty_or_nonempty_of_hausdorffEdist_ne_top (fin : hausdorffEdist s t ≠ ⊤) :
    (s = ∅ ∧ t = ∅) ∨ (s.Nonempty ∧ t.Nonempty)

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEdist s t ≠ ⊤
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

Tactic:
rcases s.eq_empty_or_nonempty with hs | hs

Result:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

case inr
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEdist s t ≠ ⊤
hs : s.Nonempty
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

Proof state:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEdist s t ≠ ⊤
hs : s.Nonempty
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

Tactic:
exact Or.inr ⟨hs, nonempty_of_hausdorffEdist_ne_top hs fin⟩

Result:
no goals

Proof state:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

Tactic:
rcases t.eq_empty_or_nonempty with ht | ht

Result:
case inl.inl
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
ht : t = ∅
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

case inl.inr
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
ht : t.Nonempty
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

Proof state:
case inl.inr
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
ht : t.Nonempty
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

Tactic:
rw [hausdorffEdist_comm] at fin

Result:
case inl.inr
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEdist t s ≠ ⊤
hs : s = ∅
ht : t.Nonempty
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

Proof state:
case inl.inl
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
ht : t = ∅
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

Tactic:
exact Or.inl ⟨hs, ht⟩

Result:
no goals

Proof state:
case inl.inr
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEdist t s ≠ ⊤
hs : s = ∅
ht : t.Nonempty
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

Tactic:
exact Or.inr ⟨nonempty_of_hausdorffEdist_ne_top ht fin, ht⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem lt_pow_self {n a : Nat} (h : 1 < a) : n < a ^ n

Proof state:
case zero
a : Nat
h : 1 < a
⊢ 0 < a ^ 0

Tactic:
exact Nat.zero_lt_one

Result:
no goals

Proof state:
n a : Nat
h : 1 < a
⊢ n < a ^ n

Tactic:
induction n with
| zero => exact Nat.zero_lt_one
| succ _ ih => exact Nat.lt_of_lt_of_le (Nat.add_lt_add_right ih 1) (Nat.pow_lt_pow_succ h)

Result:
no goals

Proof state:
case succ
a : Nat
h : 1 < a
n✝ : Nat
ih : n✝ < a ^ n✝
⊢ n✝ + 1 < a ^ (n✝ + 1)

Tactic:
exact Nat.lt_of_lt_of_le (Nat.add_lt_add_right ih 1) (Nat.pow_lt_pow_succ h)

Result:
no goals
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem pow_dvd_nthHom_sub (r : R) (i j : ℕ) (h : i ≤ j) :
    (p : ℤ) ^ i ∣ nthHom f r j - nthHom f r i

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
r : R
i j : ℕ
h : i ≤ j
f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i
⊢ ↑↑((f j) r).val - ↑↑((f i) r).val = 0

Tactic:
rw [← f_compat, RingHom.comp_apply]

Result:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
r : R
i j : ℕ
h : i ≤ j
f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i
⊢ ↑↑((f j) r).val - ↑↑((ZMod.castHom ⋯ (ZMod (p ^ i))) ((f j) r)).val = 0

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
r : R
i j : ℕ
h : i ≤ j
f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i
⊢ ↑↑((f j) r).val - ↑↑((ZMod.castHom ⋯ (ZMod (p ^ i))) ((f j) r)).val = 0

Tactic:
simp only [ZMod.cast_id, ZMod.castHom_apply, sub_self, ZMod.natCast_val, ZMod.intCast_cast]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
i j : ℕ
h : i ≤ j
⊢ ↑p ^ i ∣ nthHom f r j - nthHom f r i

Tactic:
specialize f_compat i j h

Result:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
r : R
i j : ℕ
h : i ≤ j
f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i
⊢ ↑p ^ i ∣ nthHom f r j - nthHom f r i

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
r : R
i j : ℕ
h : i ≤ j
f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i
⊢ ↑(nthHom f r j) - ↑(nthHom f r i) = 0

Tactic:
dsimp [nthHom]

Result:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
r : R
i j : ℕ
h : i ≤ j
f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i
⊢ ↑↑((f j) r).val - ↑↑((f i) r).val = 0

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
r : R
i j : ℕ
h : i ≤ j
f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i
⊢ ↑p ^ i ∣ nthHom f r j - nthHom f r i

Tactic:
rw [← Int.natCast_pow, ← ZMod.intCast_zmod_eq_zero_iff_dvd, Int.cast_sub]

Result:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
r : R
i j : ℕ
h : i ≤ j
f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i
⊢ ↑(nthHom f r j) - ↑(nthHom f r i) = 0
-- Mathlib/Algebra/Polynomial/BigOperators.lean
@[simp]
lemma natDegree_multiset_prod_X_sub_C_eq_card (s : Multiset R) :
    (s.map (X - C ·)).prod.natDegree = Multiset.card s

Proof state:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ ∀ f ∈ Multiset.map (fun x => X - C x) s, f.Monic

Tactic:
exact Multiset.forall_mem_map_iff.2 fun a _ => monic_X_sub_C a

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (Multiset.map (fun x => X - C x) s).prod.natDegree = s.card

Tactic:
rw [natDegree_multiset_prod_of_monic, Multiset.map_map]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (Multiset.map (natDegree ∘ fun x => X - C x) s).sum = s.card

case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ ∀ f ∈ Multiset.map (fun x => X - C x) s, f.Monic
-- Mathlib/Data/Seq/Computation.lean
theorem liftRel_def {R : α → β → Prop} {ca cb} :
    LiftRel R ca cb ↔ (Terminates ca ↔ Terminates cb) ∧ ∀ {a b}, a ∈ ca → b ∈ cb → R a b :=
  ⟨fun h =>
    ⟨terminates_of_liftRel h, fun {a b} ma mb => by
      let ⟨b', mb', ab⟩ := h.left ma
      rwa [mem_unique mb mb']⟩,
    fun ⟨l, r⟩ =>
    ⟨fun {_} ma =>
      let ⟨⟨b, mb⟩⟩ := l.1 ⟨⟨_, ma⟩⟩
      ⟨b, mb, r ma mb⟩,
      fun {_} mb =>
      let ⟨⟨a, ma⟩⟩ := l.2 ⟨⟨_, mb⟩⟩
      ⟨a, ma, r ma mb⟩⟩⟩

Proof state:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
h : LiftRel R ca cb
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
⊢ R a b

Tactic:
let ⟨b', mb', ab⟩ := h.left ma

Result:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
h : LiftRel R ca cb
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab : R a b'
⊢ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
h : LiftRel R ca cb
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab : R a b'
⊢ R a b

Tactic:
rwa [mem_unique mb mb']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem size_assignments_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
    (insert f c).assignments.size = f.assignments.size

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (f.insert c).assignments.size = f.assignments.size

Tactic:
simp only [insert]

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
        | none =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }
        | some (l, true) =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }
        | some (l, false) =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }).assignments.size =
    f.assignments.size

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
        | none =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }
        | some (l, true) =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }
        | some (l, false) =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }).assignments.size =
    f.assignments.size

Tactic:
split <;> simp only [Array.size_modify]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_div_nat_iff : Irrational (x / n) ↔ n ≠ 0 ∧ Irrational x

Proof state:
n : ℕ
x : ℝ
⊢ Irrational (x / ↑n) ↔ n ≠ 0 ∧ Irrational x

Tactic:
rw [← cast_natCast, irrational_div_rat_iff, Nat.cast_ne_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem Left.one_le_inv_iff : 1 ≤ a⁻¹ ↔ a ≤ 1

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a : α
⊢ a * 1 ≤ a * a⁻¹ ↔ a ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a : α
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1

Tactic:
rw [← mul_le_mul_iff_left a]

Result:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a : α
⊢ a * 1 ≤ a * a⁻¹ ↔ a ≤ 1
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem exists_word_with_prod (w : W) : ∃ n ω, ω.length = n ∧ π ω = w

Proof state:
case intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ ∃ n ω_1, ω_1.length = n ∧ cs.wordProd ω_1 = cs.wordProd ω

Tactic:
use ω.length, ω

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ ∃ n ω, ω.length = n ∧ cs.wordProd ω = w

Tactic:
rcases cs.wordProd_surjective w with ⟨ω, rfl⟩

Result:
case intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ ∃ n ω_1, ω_1.length = n ∧ cs.wordProd ω_1 = cs.wordProd ω
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
theorem limit_map_limitObjIsoLimitCompEvaluation_hom [HasLimitsOfShape J C] {i j : K}
    (F : J ⥤ K ⥤ C) (f : i ⟶ j) : (limit F).map f ≫ (limitObjIsoLimitCompEvaluation _ _).hom =
    (limitObjIsoLimitCompEvaluation _ _).hom ≫ limMap (whiskerLeft _ ((evaluation _ _).map f))

Proof state:
case w
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
j✝ : J
⊢ ((limit F).map f ≫ (limitObjIsoLimitCompEvaluation F j).hom) ≫ limit.π (F ⋙ (evaluation K C).obj j) j✝ =
    ((limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (whiskerLeft F ((evaluation K C).map f))) ≫
      limit.π (F ⋙ (evaluation K C).obj j) j✝

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limit F).map f ≫ (limitObjIsoLimitCompEvaluation F j).hom =
    (limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (whiskerLeft F ((evaluation K C).map f))

Tactic:
ext

Result:
case w
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
j✝ : J
⊢ ((limit F).map f ≫ (limitObjIsoLimitCompEvaluation F j).hom) ≫ limit.π (F ⋙ (evaluation K C).obj j) j✝ =
    ((limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (whiskerLeft F ((evaluation K C).map f))) ≫
      limit.π (F ⋙ (evaluation K C).obj j) j✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatten_mk (L : Array (Vector α n)) (h : L.size = m) :
    (mk L h).flatten =
      mk (L.map toArray).flatten (by simp [Function.comp_def, Array.map_const', h])

Proof state:
α : Type ?u.281976
n m : Nat
L : Array (Vector α n)
h : L.size = m
⊢ (Array.map toArray L).flatten.size = m * n

Tactic:
simp [Function.comp_def, Array.map_const', h]

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
L : Array (Vector α n)
h : L.size = m
⊢ { toArray := L, size_toArray := h }.flatten = { toArray := (Array.map toArray L).flatten, size_toArray := ⋯ }

Tactic:
simp [flatten]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem isUnit_iff {I : Ideal R} : IsUnit I ↔ I = ⊤ :=
  isUnit_iff_dvd_one.trans
    ((@one_eq_top R _).symm ▸
      ⟨fun h => eq_top_iff.mpr (Ideal.le_of_dvd h), fun h => ⟨⊤, by rw [mul_top, h]⟩⟩)

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
h : I = ⊤
⊢ ⊤ = I * ⊤

Tactic:
rw [mul_top, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_mkArray : (mkArray n a).toList = List.replicate n a

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ (mkArray n a).toList = List.replicate n a

Tactic:
simp only [mkArray]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
theorem lapMatrix_toLin'_apply_eq_zero_iff_forall_adj (x : V → ℝ) :
    Matrix.toLin' (G.lapMatrix ℝ) x = 0 ↔ ∀ i j : V, G.Adj i j → x i = x j

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
⊢ (toLin' (lapMatrix ℝ G)) x = 0 ↔ ∀ (i j : V), G.Adj i j → x i = x j

Tactic:
rw [← (posSemidef_lapMatrix ℝ G).toLinearMap₂'_zero_iff, star_trivial,
    lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem inv_eq_iff_mul_eq_one {φ ψ : MvPowerSeries σ k} (h : constantCoeff σ k ψ ≠ 0) :
    ψ⁻¹ = φ ↔ φ * ψ = 1

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : (constantCoeff σ k) ψ ≠ 0
⊢ ψ⁻¹ = φ ↔ φ * ψ = 1

Tactic:
rw [eq_comm, MvPowerSeries.eq_inv_iff_mul_eq_one h]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem continuous_iff (hf : IsQuotientMap f) : Continuous g ↔ Continuous (g ∘ f)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : IsQuotientMap f
⊢ Continuous g ↔ Continuous (g ∘ f)

Tactic:
rw [continuous_iff_coinduced_le, continuous_iff_coinduced_le, hf.eq_coinduced, coinduced_compose]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_union_add_ncard_inter (s t : Set α) (hs : s.Finite

Proof state:
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : autoParam t.Finite _auto✝
⊢ (s ∪ t).ncard + (s ∩ t).ncard = s.ncard + t.ncard

Tactic:
to_encard_tac

Result:
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : autoParam t.Finite _auto✝
⊢ ↑(s ∪ t).ncard + ↑(s ∩ t).ncard = ↑s.ncard + ↑t.ncard

Proof state:
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : autoParam t.Finite _auto✝
⊢ ↑(s ∪ t).ncard + ↑(s ∩ t).ncard = ↑s.ncard + ↑t.ncard

Tactic:
rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq,
(hs.subset inter_subset_left).cast_ncard_eq, encard_union_add_encard_inter]

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem range_eq_top {f : R →ₙ+* S} :
    f.range = (⊤ : NonUnitalSubring S) ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_range, coe_top]) Set.range_eq_univ

Proof state:
R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
⊢ ↑f.range = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
rw [coe_range, coe_top]

Result:
no goals
-- Mathlib/Data/Finset/Erase.lean
theorem erase_inj {x y : α} (s : Finset α) (hx : x ∈ s) : s.erase x = s.erase y ↔ x = y

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
s : Finset α
hx : x ∈ s
h : s.erase x = s.erase y
⊢ x ∉ s.erase x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
s : Finset α
hx : x ∈ s
⊢ s.erase x = s.erase y ↔ x = y

Tactic:
refine ⟨fun h => eq_of_mem_of_not_mem_erase hx ?_, congr_arg _⟩

Result:
α : Type u_1
inst✝ : DecidableEq α
x y : α
s : Finset α
hx : x ∈ s
h : s.erase x = s.erase y
⊢ x ∉ s.erase y

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
s : Finset α
hx : x ∈ s
h : s.erase x = s.erase y
⊢ x ∉ s.erase y

Tactic:
rw [← h]

Result:
α : Type u_1
inst✝ : DecidableEq α
x y : α
s : Finset α
hx : x ∈ s
h : s.erase x = s.erase y
⊢ x ∉ s.erase x
-- Mathlib/.lake/packages/batteries/Batteries/Classes/SatisfiesM.lean
theorem SatisfiesM_Option_eq : SatisfiesM (m := Option) p x ↔ ∀ a, x = some a → p a :=
  ⟨by revert x; intro | some _, ⟨some ⟨_, h⟩, rfl⟩, _, rfl => exact h,
   fun h => match x with | some a => ⟨some ⟨a, h _ rfl⟩, rfl⟩ | none => ⟨none, rfl⟩⟩

Proof state:
α✝ : Type u_1
p : α✝ → Prop
x✝³ : Option α✝
x✝² : SatisfiesM p x✝³
x✝¹ : α✝
x✝ : x✝³ = some x✝¹
val✝ : α✝
h : p val✝
⊢ p ⟨val✝, h⟩.val

Tactic:
exact h

Result:
no goals

Proof state:
α✝ : Type u_1
p : α✝ → Prop
x : Option α✝
⊢ SatisfiesM p x → ∀ (a : α✝), x = some a → p a

Tactic:
revert x

Result:
α✝ : Type u_1
p : α✝ → Prop
⊢ ∀ {x : Option α✝}, SatisfiesM p x → ∀ (a : α✝), x = some a → p a

Proof state:
α✝ : Type u_1
p : α✝ → Prop
⊢ ∀ {x : Option α✝}, SatisfiesM p x → ∀ (a : α✝), x = some a → p a

Tactic:
intro | some _, ⟨some ⟨_, h⟩, rfl⟩, _, rfl => exact h

Result:
no goals