harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem IsPartition.of_orbits :
    Setoid.IsPartition (Set.range fun a : X => orbit G a)

Proof state:
case h₂
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ ∀ (a : X), ∃ x ∈ range fun x => orbit G x, a ∈ x

Tactic:
intro x

Result:
case h₂
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
x : X
⊢ ∃ x_1 ∈ range fun x => orbit G x, x ∈ x_1

Proof state:
case h₂
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
x : X
⊢ ∃ x_1 ∈ range fun x => orbit G x, x ∈ x_1

Tactic:
exact ⟨_, ⟨x, rfl⟩, mem_orbit_self x⟩

Result:
no goals

Proof state:
case h₃
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ ∅ ∉ range fun x => orbit G x

Tactic:
rintro ⟨a, ha : orbit G a = ∅⟩

Result:
case h₃.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
ha : orbit G a = ∅
⊢ False

Proof state:
case h₃.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
ha : orbit G a = ∅
⊢ False

Tactic:
exact (MulAction.orbit_nonempty a).ne_empty ha

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ Setoid.IsPartition (range fun a => orbit G a)

Tactic:
apply orbit.pairwiseDisjoint.isPartition_of_exists_of_ne_empty

Result:
case h₂
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ ∀ (a : X), ∃ x ∈ range fun x => orbit G x, a ∈ x

case h₃
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ ∅ ∉ range fun x => orbit G x
-- Mathlib/NumberTheory/Dioph.lean
theorem diophFn_vec_comp1 {S : Set (Vector3 ℕ (succ n))} (d : Dioph S) {f : Vector3 ℕ n → ℕ}
    (df : DiophFn f) : Dioph {v : Vector3 ℕ n | (f v::v) ∈ S} :=
  Dioph.ext (diophFn_comp1 (reindex_dioph _ (none::some) d) df) (fun v => by
    dsimp
    -- Porting note: `congr` use to be enough here
    suffices ((f v ::ₒ v) ∘ none :: some) = f v :: v by rw [this]; rfl
    ext x; cases x <;> rfl)

Proof state:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
this : ((f v ::ₒ v) ∘ none :: some) = f v :: v
⊢ (f v :: v) ∈ S ↔ v ∈ {v | (f v :: v) ∈ S}

Tactic:
rfl

Result:
no goals

Proof state:
case h
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
x : Fin2 (n + 1)
⊢ ((f v ::ₒ v) ∘ none :: some) x = (f v :: v) x

Tactic:
cases x <;> rfl

Result:
no goals

Proof state:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ ((f v ::ₒ v) ∘ none :: some) = f v :: v

Tactic:
ext x

Result:
case h
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
x : Fin2 (n + 1)
⊢ ((f v ::ₒ v) ∘ none :: some) x = (f v :: v) x

Proof state:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
this : ((f v ::ₒ v) ∘ none :: some) = f v :: v
⊢ ((f v ::ₒ v) ∘ none :: some) ∈ S ↔ v ∈ {v | (f v :: v) ∈ S}

Tactic:
rw [this]

Result:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
this : ((f v ::ₒ v) ∘ none :: some) = f v :: v
⊢ (f v :: v) ∈ S ↔ v ∈ {v | (f v :: v) ∈ S}

Proof state:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ v ∈ {v | f v ::ₒ v ∈ {v | (v ∘ none :: some) ∈ S}} ↔ v ∈ {v | (f v :: v) ∈ S}

Tactic:
dsimp

Result:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ ((f v ::ₒ v) ∘ none :: some) ∈ S ↔ v ∈ {v | (f v :: v) ∈ S}

Proof state:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ ((f v ::ₒ v) ∘ none :: some) ∈ S ↔ v ∈ {v | (f v :: v) ∈ S}

Tactic:
suffices ((f v ::ₒ v) ∘ none :: some) = f v :: v by rw [this]; rfl

Result:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ ((f v ::ₒ v) ∘ none :: some) = f v :: v
-- Mathlib/Order/Atoms.lean
theorem isAtomic_dual_iff_isCoatomic [OrderTop α] : IsAtomic αᵒᵈ ↔ IsCoatomic α :=
  ⟨fun h => ⟨fun b => by apply h.eq_bot_or_exists_atom_le⟩, fun h =>
    ⟨fun b => by apply h.eq_top_or_exists_le_coatom⟩⟩

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : IsCoatomic α
b : αᵒᵈ
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
apply h.eq_top_or_exists_le_coatom

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : IsAtomic αᵒᵈ
b : α
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
apply h.eq_bot_or_exists_atom_le

Result:
no goals
-- Mathlib/Data/Nat/Find.lean
lemma find_comp_succ (h₁ : ∃ n, p n) (h₂ : ∃ n, p (n + 1)) (h0 : ¬ p 0) :
    Nat.find h₁ = Nat.find h₂ + 1

Proof state:
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
hn : 0 < Nat.find h₂ + 1
⊢ ¬p 0

case succ
p : ℕ → Prop
inst✝ : DecidablePred p
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
n✝ : ℕ
hn : n✝ + 1 < Nat.find h₂ + 1
⊢ ¬p (n✝ + 1)

Tactic:
exacts [h0, @Nat.find_min (fun n ↦ p (n + 1)) _ h₂ _ (succ_lt_succ_iff.1 hn)]

Result:
no goals

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
n : ℕ
hn : n < Nat.find h₂ + 1
⊢ ¬p n

Tactic:
cases n

Result:
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
hn : 0 < Nat.find h₂ + 1
⊢ ¬p 0

case succ
p : ℕ → Prop
inst✝ : DecidablePred p
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
n✝ : ℕ
hn : n✝ + 1 < Nat.find h₂ + 1
⊢ ¬p (n✝ + 1)

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
⊢ Nat.find h₁ = Nat.find h₂ + 1

Tactic:
refine (find_eq_iff _).2 ⟨Nat.find_spec h₂, fun n hn ↦ ?_⟩

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
n : ℕ
hn : n < Nat.find h₂ + 1
⊢ ¬p n
-- Mathlib/Analysis/Convex/Gauge.lean
theorem mem_openSegment_of_gauge_lt_one (absorbs : Absorbent ℝ s) (hgauge : gauge s x < 1) :
    ∃ y ∈ s, x ∈ openSegment ℝ 0 y

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
absorbs : Absorbent ℝ s
hgauge : gauge s x < 1
⊢ ∃ y ∈ s, x ∈ openSegment ℝ 0 y

Tactic:
rcases exists_lt_of_gauge_lt absorbs hgauge with ⟨r, hr₀, hr₁, y, hy, rfl⟩

Result:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
y : E
hy : y ∈ s
hgauge : gauge s ((fun x => r • x) y) < 1
⊢ ∃ y_1 ∈ s, (fun x => r • x) y ∈ openSegment ℝ 0 y_1

Proof state:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
y : E
hy : y ∈ s
hgauge : gauge s ((fun x => r • x) y) < 1
⊢ ∃ y_1 ∈ s, (fun x => r • x) y ∈ openSegment ℝ 0 y_1

Tactic:
refine ⟨y, hy, 1 - r, r, ?_⟩

Result:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
y : E
hy : y ∈ s
hgauge : gauge s ((fun x => r • x) y) < 1
⊢ 0 < 1 - r ∧ 0 < r ∧ 1 - r + r = 1 ∧ (1 - r) • 0 + r • y = (fun x => r • x) y

Proof state:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
y : E
hy : y ∈ s
hgauge : gauge s ((fun x => r • x) y) < 1
⊢ 0 < 1 - r ∧ 0 < r ∧ 1 - r + r = 1 ∧ (1 - r) • 0 + r • y = (fun x => r • x) y

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
theorem exists_eq_cons_of_succ (s : Sym α n.succ) : ∃ (a : α) (s' : Sym α n), s = a ::ₛ s'

Proof state:
α : Type u_1
n : ℕ
s : Sym α n.succ
⊢ ∃ a s', s = a ::ₛ s'

Tactic:
obtain ⟨a, ha⟩ := exists_mem s

Result:
case intro
α : Type u_1
n : ℕ
s : Sym α n.succ
a : α
ha : a ∈ s
⊢ ∃ a s', s = a ::ₛ s'

Proof state:
case intro
α : Type u_1
n : ℕ
s : Sym α n.succ
a : α
ha : a ∈ s
⊢ ∃ a s', s = a ::ₛ s'

Tactic:
classical exact ⟨a, s.erase a ha, (cons_erase ha).symm⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
n : ℕ
s : Sym α n.succ
a : α
ha : a ∈ s
⊢ ∃ a s', s = a ::ₛ s'

Tactic:
exact ⟨a, s.erase a ha, (cons_erase ha).symm⟩

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma map₂_id : YonedaCollection.map₂ F (𝟙 X) = id

Proof state:
case h.h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
x✝ : YonedaCollection F X
⊢ F.map (eqToHom ⋯) (id x✝).snd = (map₂ F (𝟙 X) x✝).snd

Tactic:
simp

Result:
no goals

Proof state:
case h.h.w.h.h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
x✝¹ : YonedaCollection F X
x✝ : Cᵒᵖ
a✝ : (yoneda.obj X).obj x✝
⊢ (map₂ F (𝟙 X) x✝¹).fst.app x✝ a✝ = (id x✝¹).fst.app x✝ a✝

case h.h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
x✝ : YonedaCollection F X
⊢ F.map (eqToHom ⋯) (id x✝).snd = (map₂ F (𝟙 X) x✝).snd

Tactic:
all_goals simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
⊢ map₂ F (𝟙 X) = id

Tactic:
ext

Result:
case h.h.w.h.h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
x✝¹ : YonedaCollection F X
x✝ : Cᵒᵖ
a✝ : (yoneda.obj X).obj x✝
⊢ (map₂ F (𝟙 X) x✝¹).fst.app x✝ a✝ = (id x✝¹).fst.app x✝ a✝

case h.h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
x✝ : YonedaCollection F X
⊢ F.map (eqToHom ⋯) (id x✝).snd = (map₂ F (𝟙 X) x✝).snd
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthSup_zero : expGrowthSup 0 = ⊥

Proof state:
⊢ expGrowthSup 0 = limsup (fun x => ⊥) atTop

Tactic:
apply limsup_congr

Result:
case h

⊢ ∀ᶠ (a : ℕ) in atTop, (0 a).log / ↑a = ⊥

Proof state:
case h

⊢ ∃ a, ∀ b ≥ a, ⊥ / ↑b = ⊥

Tactic:
exact ⟨1, fun n n_pos ↦ bot_div_of_pos_ne_top (Nat.cast_pos'.2 n_pos) (natCast_ne_top n)⟩

Result:
no goals

Proof state:
case h

⊢ ∀ᶠ (a : ℕ) in atTop, (0 a).log / ↑a = ⊥

Tactic:
simp only [Pi.zero_apply, log_zero, eventually_atTop]

Result:
case h

⊢ ∃ a, ∀ b ≥ a, ⊥ / ↑b = ⊥

Proof state:
⊢ expGrowthSup 0 = ⊥

Tactic:
rw [← limsup_const (f := atTop (α := ℕ)) ⊥]

Result:
⊢ expGrowthSup 0 = limsup (fun x => ⊥) atTop
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_pow (p : R[X]) (n : ℕ) :
    derivative (p ^ n) = C (n : R) * p ^ (n - 1) * derivative p :=
  Nat.casesOn n (by rw [pow_zero, derivative_one, Nat.cast_zero, C_0, zero_mul, zero_mul]) fun n =>
    by rw [p.derivative_pow_succ n, Nat.add_one_sub_one, n.cast_succ]

Proof state:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
⊢ derivative (p ^ n.succ) = C ↑n.succ * p ^ (n.succ - 1) * derivative p

Tactic:
rw [p.derivative_pow_succ n, Nat.add_one_sub_one, n.cast_succ]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ derivative (p ^ Nat.zero) = C ↑Nat.zero * p ^ (Nat.zero - 1) * derivative p

Tactic:
rw [pow_zero, derivative_one, Nat.cast_zero, C_0, zero_mul, zero_mul]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_strictAnti : StrictAnti (Inv.inv : ℝ≥0∞ → ℝ≥0∞)

Proof state:
⊢ StrictAnti Inv.inv

Tactic:
intro a b h

Result:
a b : ℝ≥0∞
h : a < b
⊢ b⁻¹ < a⁻¹

Proof state:
case intro
b : ℝ≥0∞
a : ℝ≥0
h : ↑a < b
⊢ b⁻¹ < (↑a)⁻¹

Tactic:
induction b

Result:
case intro.top
a : ℝ≥0
h : ↑a < ⊤
⊢ ⊤⁻¹ < (↑a)⁻¹

case intro.coe
a x✝ : ℝ≥0
h : ↑a < ↑x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹

Proof state:
a b : ℝ≥0∞
h : a < b
⊢ b⁻¹ < a⁻¹

Tactic:
lift a to ℝ≥0 using h.ne_top

Result:
case intro
b : ℝ≥0∞
a : ℝ≥0
h : ↑a < b
⊢ b⁻¹ < (↑a)⁻¹

Proof state:
case intro.coe
a x✝ : ℝ≥0
h : a < x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹

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

Result:
case intro.coe.inl
x✝ : ℝ≥0
h : 0 < x✝
⊢ (↑x✝)⁻¹ < (↑0)⁻¹

case intro.coe.inr
a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ (↑x✝)⁻¹ < (↑a)⁻¹

Proof state:
case intro.top
a : ℝ≥0
h : ↑a < ⊤
⊢ ⊤⁻¹ < (↑a)⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case intro.coe
a x✝ : ℝ≥0
h : ↑a < ↑x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹

Tactic:
rw [coe_lt_coe] at h

Result:
case intro.coe
a x✝ : ℝ≥0
h : a < x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹

Proof state:
case intro.coe.inr
a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ x✝⁻¹ < a⁻¹

Tactic:
exact NNReal.inv_lt_inv ha h

Result:
no goals

Proof state:
case intro.coe.inr
a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ (↑x✝)⁻¹ < (↑a)⁻¹

Tactic:
rw [← coe_inv h.ne_bot, ← coe_inv ha, coe_lt_coe]

Result:
case intro.coe.inr
a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ x✝⁻¹ < a⁻¹

Proof state:
case intro.coe.inl
x✝ : ℝ≥0
h : 0 < x✝
⊢ (↑x✝)⁻¹ < (↑0)⁻¹

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiff.div_const {f : E → 𝕜'} {n} (hf : ContDiff 𝕜 n f) (c : 𝕜') :
    ContDiff 𝕜 n fun x => f x / c

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_6
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
n : WithTop ℕ∞
hf : ContDiff 𝕜 n f
c : 𝕜'
⊢ ContDiff 𝕜 n fun x => f x / c

Tactic:
simpa only [div_eq_mul_inv] using hf.mul contDiff_const

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem prod_le_pow_card (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, f x ≤ n) :
    s.prod f ≤ n ^ #s

Proof state:
case refine_1
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ ∀ x ∈ Multiset.map f s.val, x ≤ n

Tactic:
simpa using h

Result:
no goals

Proof state:
case refine_2
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ n ^ (Multiset.map f s.val).card ≤ n ^ #s

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ s.prod f ≤ n ^ #s

Tactic:
refine (Multiset.prod_le_pow_card (s.val.map f) n ?_).trans ?_

Result:
case refine_1
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ ∀ x ∈ Multiset.map f s.val, x ≤ n

case refine_2
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ n ^ (Multiset.map f s.val).card ≤ n ^ #s
-- Mathlib/RingTheory/Localization/Ideal.lean
lemma _root_.NoZeroSMulDivisors_of_isLocalization (Rₚ Sₚ : Type*) [CommRing Rₚ] [CommRing Sₚ]
    [Algebra R Rₚ] [Algebra R Sₚ] [Algebra S Sₚ] [Algebra Rₚ Sₚ] [IsScalarTower R S Sₚ]
    [IsScalarTower R Rₚ Sₚ] {M : Submonoid R} (hM : M ≤ R⁰) [IsLocalization M Rₚ]
    [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [NoZeroSMulDivisors R S] [IsDomain S] :
    NoZeroSMulDivisors Rₚ Sₚ

Proof state:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
⊢ NoZeroSMulDivisors Rₚ Sₚ

Tactic:
have : IsDomain Sₚ := IsLocalization.isDomain_of_le_nonZeroDivisors S e

Result:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this : IsDomain Sₚ
⊢ NoZeroSMulDivisors Rₚ Sₚ

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : a * x = 0
⊢ ∃ a ∈ M, a * x = 0

Tactic:
exact ⟨a, ha, H⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem toDual_linearCombination_left (f : ι →₀ R) (i : ι) :
    b.toDual (Finsupp.linearCombination R b f) (b i) = f i

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (b.toDual ((Finsupp.linearCombination R ⇑b) f)) (b i) = f i

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.sum, _root_.map_sum, LinearMap.sum_apply]

Result:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ d ∈ f.support, (b.toDual (f d • b d)) (b i) = f i

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ d ∈ f.support, (b.toDual (f d • b d)) (b i) = f i

Tactic:
simp_rw [LinearMap.map_smul, LinearMap.smul_apply, toDual_apply, smul_eq_mul, mul_boole,
  Finset.sum_ite_eq']

Result:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (if i ∈ f.support then f i else 0) = f i

Proof state:
case pos
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : i ∈ f.support
⊢ f i = f i

Tactic:
rfl

Result:
no goals

Proof state:
case neg
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : i ∉ f.support
⊢ 0 = f i

Tactic:
rw [Finsupp.not_mem_support_iff.mp h]

Result:
no goals

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (if i ∈ f.support then f i else 0) = f i

Tactic:
split_ifs with h

Result:
case pos
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : i ∈ f.support
⊢ f i = f i

case neg
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : i ∉ f.support
⊢ 0 = f i
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem isAlgebraic_of_isAlgebraic_bot {x : S} (halg : _root_.IsAlgebraic (⊥ : Subalgebra R S) x) :
    _root_.IsAlgebraic R x :=
  halg.of_ringHom_of_comp_eq (algebraMap R (⊥ : Subalgebra R S))
    (RingHom.id S) (by rintro ⟨_, r, rfl⟩; exact ⟨r, rfl⟩) Function.injective_id rfl

Proof state:
R : Type u
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
halg : _root_.IsAlgebraic (↥⊥) x
⊢ Function.Surjective ⇑(algebraMap R ↥⊥)

Tactic:
rintro ⟨_, r, rfl⟩

Result:
case mk.intro
R : Type u
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
halg : _root_.IsAlgebraic (↥⊥) x
r : R
⊢ ∃ a, (algebraMap R ↥⊥) a = ⟨(Algebra.ofId R S).toRingHom r, ⋯⟩

Proof state:
case mk.intro
R : Type u
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
halg : _root_.IsAlgebraic (↥⊥) x
r : R
⊢ ∃ a, (algebraMap R ↥⊥) a = ⟨(Algebra.ofId R S).toRingHom r, ⋯⟩

Tactic:
exact ⟨r, rfl⟩

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem sdiff_insert (s t : Finset α) (x : α) : s \ insert x t = (s \ t).erase x

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

Tactic:
simp_rw [← sdiff_singleton_eq_erase, insert_eq, sdiff_sdiff_left', sdiff_union_distrib,
  inter_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem intervalIntegrable_inv_one_add_sq :
    IntervalIntegrable (fun x : ℝ => (↑1 + x ^ 2)⁻¹) μ a b

Proof state:
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
⊢ IntervalIntegrable (fun x => (1 + x ^ 2)⁻¹) μ a b

Tactic:
field_simp

Result:
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
⊢ IntervalIntegrable (fun x => 1 / (1 + x ^ 2)) μ a b

Proof state:
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
⊢ IntervalIntegrable (fun x => 1 / (1 + x ^ 2)) μ a b

Tactic:
exact mod_cast intervalIntegrable_one_div_one_add_sq

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma map_zero : Kernel.map (0 : Kernel α β) f = 0

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
hf : ¬Measurable f
⊢ ((map 0 f) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
simp [map_of_not_measurable _ hf, map_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
⊢ map 0 f = 0

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((map 0 f) a✝¹) s✝ = (0 a✝¹) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((map 0 f) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
by_cases hf : Measurable f

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
hf : Measurable f
⊢ ((map 0 f) a✝¹) s✝ = (0 a✝¹) s✝

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
hf : ¬Measurable f
⊢ ((map 0 f) a✝¹) s✝ = (0 a✝¹) s✝

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
hf : Measurable f
⊢ ((map 0 f) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
simp [map_apply, hf]

Result:
no goals