harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/ContinuousOn.lean
theorem IsOpenMap.continuousOn_image_of_leftInvOn {f : α → β} {s : Set α}
    (h : IsOpenMap (s.restrict f)) {finv : β → α} (hleft : LeftInvOn finv f s) :
    ContinuousOn finv (f '' s)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.restrict f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ IsOpen (s.restrict f '' (Subtype.val ⁻¹' t))

Tactic:
exact h _ (ht.preimage continuous_subtype_val)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.restrict f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ finv ⁻¹' t ∩ f '' s = f '' (t ∩ s) ∩ f '' s

Tactic:
rw [inter_eq_self_of_subset_left (image_subset f inter_subset_right), hleft.image_inter']

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.restrict f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ IsOpen (f '' (t ∩ s))

Tactic:
rw [← image_restrict]

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.restrict f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ IsOpen (s.restrict f '' (Subtype.val ⁻¹' t))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.restrict f)
finv : β → α
hleft : LeftInvOn finv f s
⊢ ContinuousOn finv (f '' s)

Tactic:
refine continuousOn_iff'.2 fun t ht => ⟨f '' (t ∩ s), ?_, ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.restrict f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ IsOpen (f '' (t ∩ s))

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.restrict f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ finv ⁻¹' t ∩ f '' s = f '' (t ∩ s) ∩ f '' s
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem div_dvd_of_dvd {p q : R} (hpq : q ∣ p) : p / q ∣ p

Proof state:
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
⊢ p / q ∣ p

Tactic:
rw [hpq]

Result:
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
⊢ 0 / q ∣ 0

Proof state:
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
⊢ 0 / q ∣ 0

Tactic:
exact dvd_zero _

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p / q ∣ p

Tactic:
use q

Result:
case h
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p = p / q * q

Proof state:
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
⊢ p / q ∣ p

Tactic:
by_cases hq : q = 0

Result:
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : q = 0
⊢ p / q ∣ p

case neg
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p / q ∣ p

Proof state:
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : q = 0
⊢ p / q ∣ p

Tactic:
rw [hq, zero_dvd_iff] at hpq

Result:
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
⊢ p / q ∣ p

Proof state:
case h
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p = p / q * q

Tactic:
rw [mul_comm, ← EuclideanDomain.mul_div_assoc _ hpq, mul_comm, mul_div_cancel_right₀ _ hq]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_finset_product₃ {γ : Type*} (s : Finset (α × β × γ)) (f : α × β × γ → M) :
    (∏ᶠ (abc) (_ : abc ∈ s), f abc) = ∏ᶠ (a) (b) (c) (_ : (a, b, c) ∈ s), f (a, b, c)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc = ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)

Tactic:
classical
  rw [finprod_mem_finset_product']
  simp_rw [finprod_mem_finset_product']
  simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc = ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)

Tactic:
rw [finprod_mem_finset_product']

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (a : α) (b : β × γ) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s)), f (a, b) =
    ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (a : α) (b : β × γ) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s)), f (a, b) =
    ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)

Tactic:
simp_rw [finprod_mem_finset_product']

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (a : α) (a_1 : β) (b : γ) (_ :
      b ∈
        Finset.image Prod.snd
          (Finset.filter (fun ab => ab.1 = a_1) (Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s)))),
      f (a, a_1, b) =
    ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (a : α) (a_1 : β) (b : γ) (_ :
      b ∈
        Finset.image Prod.snd
          (Finset.filter (fun ab => ab.1 = a_1) (Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s)))),
      f (a, a_1, b) =
    ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem comp' {n m f g} (hf : @Primrec' m f) (hg : @Vec n m g) : Primrec' fun v => f (g v) :=
  (hf.comp _ hg).of_eq fun v => by simp

Proof state:
n m : ℕ
f : List.Vector ℕ m → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Primrec' f
hg : Vec g
v : List.Vector ℕ n
⊢ f (ofFn fun i => (g v).get i) = f (g v)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/PEquiv.lean
theorem inj (f : α ≃. β) {a₁ a₂ : α} {b : β} (h₁ : b ∈ f a₁) (h₂ : b ∈ f a₂) :
    a₁ = a₂

Proof state:
α : Type u
β : Type v
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : b ∈ f a₁
h₂ : b ∈ f a₂
⊢ a₁ = a₂

Tactic:
rw [← mem_iff_mem] at *

Result:
α : Type u
β : Type v
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : a₁ ∈ f.symm b
h₂ : a₂ ∈ f.symm b
⊢ a₁ = a₂

Proof state:
α : Type u
β : Type v
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : a₁ ∈ f.symm b
h₂ : a₂ ∈ f.symm b
⊢ a₁ = a₂

Tactic:
cases h : f.symm b <;> simp_all

Result:
no goals
-- Mathlib/Data/List/Scan.lean
theorem scanr_cons (f : α → β → β) (b : β) (a : α) (l : List α) :
    scanr f b (a :: l) = foldr f b (a :: l) :: scanr f b l

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
a : α
l : List α
⊢ f a (foldr (fun a x => (f a x.fst, x.fst :: x.snd)) (b, []) l).fst = f a (foldr f b l)

Tactic:
induction l generalizing a with
| nil => rfl
| cons hd tl ih => simp only [foldr, ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β → β
b : β
hd : α
tl : List α
ih : ∀ (a : α), f a (foldr (fun a x => (f a x.fst, x.fst :: x.snd)) (b, []) tl).fst = f a (foldr f b tl)
a : α
⊢ f a (foldr (fun a x => (f a x.fst, x.fst :: x.snd)) (b, []) (hd :: tl)).fst = f a (foldr f b (hd :: tl))

Tactic:
simp only [foldr, ih]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
a : α
l : List α
⊢ scanr f b (a :: l) = foldr f b (a :: l) :: scanr f b l

Tactic:
simp only [scanr, foldr, cons.injEq, and_true]

Result:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
a : α
l : List α
⊢ f a (foldr (fun a x => (f a x.fst, x.fst :: x.snd)) (b, []) l).fst = f a (foldr f b l)

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β → β
b : β
a : α
⊢ f a (foldr (fun a x => (f a x.fst, x.fst :: x.snd)) (b, []) []).fst = f a (foldr f b [])

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Units.lean
theorem eq_top_of_norm_lt_one (I : Ideal R) {x : R} (hxI : x ∈ I) (hx : ‖1 - x‖ < 1) : I = ⊤ :=
  let u := Units.oneSub (1 - x) hx
  I.eq_top_iff_one.mpr <| by
    simpa only [show u.inv * x = 1 by simp [u]] using I.mul_mem_left u.inv hxI

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
I : Ideal R
x : R
hxI : x ∈ I
hx : ‖1 - x‖ < 1
u : Rˣ := Units.oneSub (1 - x) hx
⊢ u.inv * x = 1

Tactic:
simp [u]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
I : Ideal R
x : R
hxI : x ∈ I
hx : ‖1 - x‖ < 1
u : Rˣ := Units.oneSub (1 - x) hx
⊢ 1 ∈ I

Tactic:
simpa only [show u.inv * x = 1 by simp [u]] using I.mul_mem_left u.inv hxI

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
/-- Every Yoneda-presheaf is a sheaf for the regular topology. -/
lemma isSheaf_yoneda_obj [Preregular C] (W : C)  :
    Presieve.IsSheaf (regularTopology C) (yoneda.obj W)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W : C
⊢ IsSheaf (regularTopology C) (yoneda.obj W)

Tactic:
rw [regularTopology, isSheaf_coverage]

Result:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W : C
⊢ ∀ {X : C}, ∀ R ∈ (regularCoverage C).covering X, IsSheafFor (yoneda.obj W) R

Proof state:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X : C
S : Presieve X
w✝ : C
hS : ∃ f, (S = ofArrows (fun x => w✝) fun x => f) ∧ EffectiveEpi f
⊢ IsSheafFor (yoneda.obj W) S

Tactic:
have : S.regular := ⟨_, hS⟩

Result:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X : C
S : Presieve X
w✝ : C
hS : ∃ f, (S = ofArrows (fun x => w✝) fun x => f) ∧ EffectiveEpi f
this : S.regular
⊢ IsSheafFor (yoneda.obj W) S

Proof state:
case intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x => Y) fun x => f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone
x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Tactic:
let x_ext := Presieve.FamilyOfElements.sieveExtend x

Result:
case intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x => Y) fun x => f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone
x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)
hx : x.Compatible
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows := x.sieveExtend
⊢ ∃! t, x.IsAmalgamation t

Proof state:
case intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x => Y) fun x => f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone
⊢ IsSheafFor (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)

Tactic:
intro x hx

Result:
case intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x => Y) fun x => f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone
x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t
-- Mathlib/GroupTheory/Sylow.lean
/-- A special case of **Sylow's first theorem**. If `G` is a `p`-group and `H` a subgroup of size at
least `k` then there is a subgroup of `H` of cardinality between `k / p` and `k`. -/
lemma exists_subgroup_le_card_le {k p : ℕ} (hp : p.Prime) (h : IsPGroup p G) {H : Subgroup G}
    (hk : k ≤ Nat.card H) (hk₀ : k ≠ 0) : ∃ H' ≤ H, Nat.card H' ≤ k ∧ k < p * Nat.card H'

Proof state:
case intro.intro.intro.intro
G : Type u
inst✝ : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
H' : Subgroup G
H'H : H' ≤ H
H'card : Nat.card ↥H' = p ^ m
⊢ ∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'

Tactic:
refine ⟨H', H'H, ?_⟩

Result:
case intro.intro.intro.intro
G : Type u
inst✝ : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
H' : Subgroup G
H'H : H' ≤ H
H'card : Nat.card ↥H' = p ^ m
⊢ Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'

Proof state:
case intro.intro
G : Type u
inst✝ : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
⊢ ∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'

Tactic:
obtain ⟨H', H'H, H'card⟩ := exists_subgroup_le_card_pow_prime_of_le_card hp h (hmk.trans hk)

Result:
case intro.intro.intro.intro
G : Type u
inst✝ : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
H' : Subgroup G
H'H : H' ≤ H
H'card : Nat.card ↥H' = p ^ m
⊢ ∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'

Proof state:
case intro.intro.intro.intro
G : Type u
inst✝ : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
H' : Subgroup G
H'H : H' ≤ H
H'card : Nat.card ↥H' = p ^ m
⊢ Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'

Tactic:
simpa only [pow_succ', H'card] using And.intro hmk hkm

Result:
no goals

Proof state:
G : Type u
inst✝ : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card ↥H
hk₀ : k ≠ 0
⊢ ∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'

Tactic:
obtain ⟨m, hmk, hkm⟩ : ∃ s, p ^ s ≤ k ∧ k < p ^ (s + 1) :=
  exists_nat_pow_near (Nat.one_le_iff_ne_zero.2 hk₀) hp.one_lt

Result:
case intro.intro
G : Type u
inst✝ : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
⊢ ∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_cons {l : List α} {a : α} {f : (i : Nat) → α → (h : i < l.length + 1) → β} :
    mapFinIdx (a :: l) f = f 0 a (by omega) :: mapFinIdx l (fun i a h => f (i + 1) a (by omega))

Proof state:
α : Type ?u.21452
β : Type ?u.21509
l : List α
a✝ : α
f : (i : Nat) → α → i < l.length + 1 → β
i : Nat
a : α
h : i < l.length
⊢ i + 1 < l.length + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
a : α
f : (i : Nat) → α → i < l.length + 1 → β
⊢ (a :: l).mapFinIdx f = f 0 a ⋯ :: l.mapFinIdx fun i a h => f (i + 1) a ⋯

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
β : Type u_2
l : List α
a : α
f : (i : Nat) → α → i < l.length + 1 → β
⊢ ((a :: l).mapFinIdx f).length = (f 0 a ⋯ :: l.mapFinIdx fun i a h => f (i + 1) a ⋯).length

case h
α : Type u_1
β : Type u_2
l : List α
a : α
f : (i : Nat) → α → i < l.length + 1 → β
⊢ ∀ (i : Nat) (h₁ : i < ((a :: l).mapFinIdx f).length)
    (h₂ : i < (f 0 a ⋯ :: l.mapFinIdx fun i a h => f (i + 1) a ⋯).length),
    ((a :: l).mapFinIdx f)[i] = (f 0 a ⋯ :: l.mapFinIdx fun i a h => f (i + 1) a ⋯)[i]

Proof state:
case hl
α : Type u_1
β : Type u_2
l : List α
a : α
f : (i : Nat) → α → i < l.length + 1 → β
⊢ ((a :: l).mapFinIdx f).length = (f 0 a ⋯ :: l.mapFinIdx fun i a h => f (i + 1) a ⋯).length

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
l : List α
a : α
f : (i : Nat) → α → i < l.length + 1 → β
⊢ ∀ (i : Nat) (h₁ : i < ((a :: l).mapFinIdx f).length)
    (h₂ : i < (f 0 a ⋯ :: l.mapFinIdx fun i a h => f (i + 1) a ⋯).length),
    ((a :: l).mapFinIdx f)[i] = (f 0 a ⋯ :: l.mapFinIdx fun i a h => f (i + 1) a ⋯)[i]

Tactic:
rintro (_|i) h₁ h₂ <;> simp

Result:
no goals

Proof state:
α : Type ?u.21452
β : Type ?u.21509
l : List α
a : α
f : (i : Nat) → α → i < l.length + 1 → β
⊢ 0 < l.length + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem ball_smul (p : Seminorm 𝕜 E) {c : NNReal} (hc : 0 < c) (r : ℝ) (x : E) :
    (c • p).ball x r = p.ball x (r / c)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x : E
⊢ (c • p).ball x r = p.ball x (r / ↑c)

Tactic:
ext

Result:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x✝ : E
⊢ x✝ ∈ (c • p).ball x r ↔ x✝ ∈ p.ball x (r / ↑c)

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x✝ : E
⊢ x✝ ∈ (c • p).ball x r ↔ x✝ ∈ p.ball x (r / ↑c)

Tactic:
rw [mem_ball, mem_ball, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
  lt_div_iff₀ (NNReal.coe_pos.mpr hc)]

Result:
no goals
-- Mathlib/Data/List/Duplicate.lean
theorem duplicate_iff_sublist : x ∈+ l ↔ [x, x] <+ l

Proof state:
α : Type u_1
l : List α
x : α
⊢ x ∈+ l ↔ [x, x] <+ l

Tactic:
induction' l with y l IH

Result:
case nil
α : Type u_1
l : List α
x : α
⊢ x ∈+ [] ↔ [x, x] <+ []

case cons
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Proof state:
case nil
α : Type u_1
l : List α
x : α
⊢ x ∈+ [] ↔ [x, x] <+ []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Tactic:
by_cases hx : x = y

Result:
case pos
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Proof state:
case neg.cons₂
α : Type u_1
l✝ : List α
x : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = x
a✝ : [x] <+ l
⊢ [x, x] <+ l

Tactic:
contradiction

Result:
no goals

Proof state:
case pos
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Tactic:
simp [hx, cons_sublist_cons, singleton_sublist]

Result:
no goals

Proof state:
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ [x, x] <+ l ↔ [x, x] <+ y :: l

Tactic:
refine ⟨sublist_cons_of_sublist y, fun h => ?_⟩

Result:
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
h : [x, x] <+ y :: l
⊢ [x, x] <+ l

Proof state:
case neg.cons
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
a✝ : [x, x] <+ l
⊢ [x, x] <+ l

Tactic:
assumption

Result:
no goals

Proof state:
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
h : [x, x] <+ y :: l
⊢ [x, x] <+ l

Tactic:
cases h

Result:
case neg.cons
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
a✝ : [x, x] <+ l
⊢ [x, x] <+ l

case neg.cons₂
α : Type u_1
l✝ : List α
x : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = x
a✝ : [x] <+ l
⊢ [x, x] <+ l

Proof state:
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Tactic:
rw [duplicate_cons_iff_of_ne hx, IH]

Result:
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ [x, x] <+ l ↔ [x, x] <+ y :: l
-- Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
theorem AEFinStronglyMeasurable.ae_nonneg_of_forall_setIntegral_nonneg {f : α → ℝ}
    (hf : AEFinStronglyMeasurable f μ)
    (hf_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn f s μ)
    (hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → 0 ≤ ∫ x in s, f x ∂μ) : 0 ≤ᵐ[μ] f

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμts : μ (s ∩ t) < ⊤
⊢ Integrable f (μ.restrict (s ∩ t))

Tactic:
exact hf_int_finite (s ∩ t) (hs.inter hf.measurableSet) hμts

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_rev (x : BitVec w) (i : Fin w) :
    x.getMsbD i.rev = x.getLsbD i

Proof state:
w : Nat
x : BitVec w
i : Fin w
⊢ x.getLsbD ↑i.rev.rev = x.getLsbD ↑i

Tactic:
simp only [Fin.rev]

Result:
w : Nat
x : BitVec w
i : Fin w
⊢ x.getLsbD (w - (w - (↑i + 1) + 1)) = x.getLsbD ↑i

Proof state:
case e_i
w : Nat
x : BitVec w
i : Fin w
⊢ w - (w - (↑i + 1) + 1) = ↑i

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Fin w
⊢ x.getLsbD (w - (w - (↑i + 1) + 1)) = x.getLsbD ↑i

Tactic:
congr

Result:
case e_i
w : Nat
x : BitVec w
i : Fin w
⊢ w - (w - (↑i + 1) + 1) = ↑i

Proof state:
w : Nat
x : BitVec w
i : Fin w
⊢ x.getMsbD ↑i.rev = x.getLsbD ↑i

Tactic:
simp only [← getLsbD_rev]

Result:
w : Nat
x : BitVec w
i : Fin w
⊢ x.getLsbD ↑i.rev.rev = x.getLsbD ↑i
-- Mathlib/NumberTheory/FactorisationProperties.lean
lemma deficient_iff_not_abundant_and_not_perfect (hn : n ≠ 0) :
    Deficient n ↔ ¬ Abundant n ∧ ¬ Perfect n

Proof state:
n : ℕ
hn : n ≠ 0
⊢ n.Deficient ↔ ¬n.Abundant ∧ ¬n.Perfect

Tactic:
dsimp only [Perfect, Abundant, Deficient]

Result:
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.properDivisors, i < n ↔ ¬n < ∑ i ∈ n.properDivisors, i ∧ ¬(∑ i ∈ n.properDivisors, i = n ∧ 0 < n)

Proof state:
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.properDivisors, i < n ↔ ¬n < ∑ i ∈ n.properDivisors, i ∧ ¬(∑ i ∈ n.properDivisors, i = n ∧ 0 < n)

Tactic:
omega

Result:
no goals
-- Mathlib/Data/ZMod/ValMinAbs.lean
lemma natAbs_valMinAbs_le [NeZero n] (x : ZMod n) : x.valMinAbs.natAbs ≤ n / 2

Proof state:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ ↑x.valMinAbs.natAbs * 2 ≤ ↑n

Tactic:
rcases x.valMinAbs.natAbs_eq with h | h

Result:
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = ↑x.valMinAbs.natAbs
⊢ ↑x.valMinAbs.natAbs * 2 ≤ ↑n

case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = -↑x.valMinAbs.natAbs
⊢ ↑x.valMinAbs.natAbs * 2 ≤ ↑n

Proof state:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ x.valMinAbs.natAbs ≤ n / 2

Tactic:
rw [Nat.le_div_two_iff_mul_two_le]

Result:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ ↑x.valMinAbs.natAbs * 2 ≤ ↑n

Proof state:
case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = -↑x.valMinAbs.natAbs
⊢ ↑x.valMinAbs.natAbs * 2 ≤ ↑n

Tactic:
rw [← neg_le_neg_iff, ← neg_mul, ← h]

Result:
case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = -↑x.valMinAbs.natAbs
⊢ -↑n ≤ x.valMinAbs * 2

Proof state:
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = ↑x.valMinAbs.natAbs
⊢ x.valMinAbs * 2 ≤ ↑n

Tactic:
exact x.valMinAbs_mem_Ioc.2

Result:
no goals

Proof state:
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = ↑x.valMinAbs.natAbs
⊢ ↑x.valMinAbs.natAbs * 2 ≤ ↑n

Tactic:
rw [← h]

Result:
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = ↑x.valMinAbs.natAbs
⊢ x.valMinAbs * 2 ≤ ↑n

Proof state:
case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = -↑x.valMinAbs.natAbs
⊢ -↑n ≤ x.valMinAbs * 2

Tactic:
exact x.valMinAbs_mem_Ioc.1.le

Result:
no goals