harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma nonsingular_smul (P : Fin 3 → R) {u : R} (hu : IsUnit u) :
    W'.Nonsingular (u • P) ↔ W'.Nonsingular P :=
  have hP {u : R} (hu : IsUnit u) {P : Fin 3 → R} (hP : W'.Nonsingular <| u • P) :
      W'.Nonsingular P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) = 0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 = 0 ∧
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) =
        0
⊢ W'.a₁ * (u * P y) * (u * P z) - (3 * (u * P x) ^ 2 + 2 * W'.a₂ * (u * P x) * (u * P z) + W'.a₄ * (u * P z) ^ 2) = 0

Tactic:
linear_combination (norm := ring1) u ^ 2 * hP'.left

Result:
no goals

Proof state:
case intro
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z + W'.a₄ * (u • P) z ^ 2) ≠ 0 ∨
    2 * (u • P) y * (u • P) z + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 2 ≠ 0 ∨
      (u • P) y ^ 2 + W'.a₁ * (u • P) x * (u • P) y + 2 * W'.a₃ * (u • P) y * (u • P) z -
          (W'.a₂ * (u • P) x ^ 2 + 2 * W'.a₄ * (u • P) x * (u • P) z + 3 * W'.a₆ * (u • P) z ^ 2) ≠
        0
⊢ W'.Nonsingular P

Tactic:
refine (nonsingular_iff P).mpr ⟨(equation_smul P hu).mp hP, ?_⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z + W'.a₄ * (u • P) z ^ 2) ≠ 0 ∨
    2 * (u • P) y * (u • P) z + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 2 ≠ 0 ∨
      (u • P) y ^ 2 + W'.a₁ * (u • P) x * (u • P) y + 2 * W'.a₃ * (u • P) y * (u • P) z -
          (W'.a₂ * (u • P) x ^ 2 + 2 * W'.a₄ * (u • P) x * (u • P) z + 3 * W'.a₆ * (u • P) z ^ 2) ≠
        0
⊢ W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) ≠ 0 ∨
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 ≠ 0 ∨
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) ≠
        0
-- Mathlib/RingTheory/Localization/Away/Lemmas.lean
lemma span_range_mulNumerator_eq_top {s : Set R}
    (hsone : Ideal.span s = ⊤) {Rₜ : s → Type*} [∀ t, CommRing (Rₜ t)] [∀ t, Algebra R (Rₜ t)]
    [∀ t, IsLocalization.Away t.val (Rₜ t)]
    {p : (t : s) → Set (Rₜ t)} (htone : ∀ (r : s), Ideal.span (p r) = ⊤) :
    Ideal.span (Set.range (IsLocalization.Away.mulNumerator s p)) = ⊤

Proof state:
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
x : Rₜ ⟨a, ha⟩
hx : x ∈ p ⟨a, ha⟩
⊢ ∃ z, x = mk' (Rₜ ⟨a, ha⟩) (a * (sec a x).1) z

Tactic:
use ⟨a ^ ((IsLocalization.Away.sec a x).2 + 1), _, rfl⟩

Result:
case h
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
x : Rₜ ⟨a, ha⟩
hx : x ∈ p ⟨a, ha⟩
⊢ x = mk' (Rₜ ⟨a, ha⟩) (a * (sec a x).1) ⟨a ^ ((sec a x).2 + 1), ⋯⟩

Proof state:
case h
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
y : R
hy : y ∈ Ideal.span (Set.range (mulNumerator s p))
m n : ℕ
hc : a ^ n * a ^ m = a ^ n * y
⊢ a ^ (n + m) ∈ Ideal.span (Set.range (mulNumerator s p))

Tactic:
simpa [pow_add, hc] using Ideal.mul_mem_left _ _ hy

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
@[simp] lemma coe_mk (f : A → M)
    (map_zero_eq_one' : f 0 = 1) (map_add_eq_mul' : ∀ a b : A, f (a + b) = f a * f b) :
    AddChar.mk f map_zero_eq_one' map_add_eq_mul' = f

Proof state:
A : Type u_1
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : Monoid M
f : A → M
map_zero_eq_one' : f 0 = 1
map_add_eq_mul' : ∀ (a b : A), f (a + b) = f a * f b
⊢ ⇑{ toFun := f, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' } = f

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma truncatedInf_union_of_not_mem (hs : a ∉ upperClosure s) (ht : a ∉ upperClosure t) :
    truncatedInf (s ∪ t) a = ⊥ :=
  truncatedInf_of_not_mem <| by rw [coe_union, upperClosure_union]; exact fun h ↦ h.elim hs ht

Proof state:
α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∉ upperClosure ↑s
ht : a ∉ upperClosure ↑t
⊢ a ∉ upperClosure ↑(s ∪ t)

Tactic:
rw [coe_union, upperClosure_union]

Result:
α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∉ upperClosure ↑s
ht : a ∉ upperClosure ↑t
⊢ a ∉ upperClosure ↑s ⊓ upperClosure ↑t

Proof state:
α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∉ upperClosure ↑s
ht : a ∉ upperClosure ↑t
⊢ a ∉ upperClosure ↑s ⊓ upperClosure ↑t

Tactic:
exact fun h ↦ h.elim hs ht

Result:
no goals
-- Mathlib/Analysis/PSeriesComplex.lean
lemma Complex.summable_one_div_nat_cpow {p : ℂ} :
    Summable (fun n : ℕ ↦ 1 / (n : ℂ) ^ p) ↔ 1 < re p

Proof state:
p : ℂ
⊢ (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p.re

Tactic:
rw [← Real.summable_one_div_nat_rpow, ← summable_nat_add_iff 1 (G := ℝ),
  ← summable_nat_add_iff 1 (G := ℂ), ← summable_norm_iff]

Result:
p : ℂ
⊢ (Summable fun x => ‖1 / ↑(x + 1) ^ p‖) ↔ Summable fun n => 1 / ↑(n + 1) ^ p.re

Proof state:
p : ℂ
⊢ (Summable fun x => ‖1 / ↑(x + 1) ^ p‖) ↔ Summable fun n => 1 / ↑(n + 1) ^ p.re

Tactic:
simp only [norm_div, norm_one, ← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos
  (Nat.cast_pos.mpr <| Nat.succ_pos _)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem enumFrom_eq_map_enum (l : List α) (n : Nat) :
    enumFrom n l = (enum l).map (Prod.map (· + n) id)

Proof state:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (n : Nat), enumFrom n xs = map (Prod.map (fun x => x + n) id) xs.enum
n : Nat
⊢ ∀ (a : Nat) (b : α), (a, b) ∈ xs.enum → a + (n + 1) = a + 1 + n

Tactic:
intro a b _

Result:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (n : Nat), enumFrom n xs = map (Prod.map (fun x => x + n) id) xs.enum
n a : Nat
b : α
a✝ : (a, b) ∈ xs.enum
⊢ a + (n + 1) = a + 1 + n

Proof state:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (n : Nat), enumFrom n xs = map (Prod.map (fun x => x + n) id) xs.enum
n : Nat
⊢ enumFrom n (x :: xs) = map (Prod.map (fun x => x + n) id) (x :: xs).enum

Tactic:
simp only [enumFrom_cons, ih, enum_cons, map_cons, Prod.map_apply, Nat.zero_add, id_eq, map_map,
  cons.injEq, map_inj_left, Function.comp_apply, Prod.forall, Prod.mk.injEq, and_true, true_and]

Result:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (n : Nat), enumFrom n xs = map (Prod.map (fun x => x + n) id) xs.enum
n : Nat
⊢ ∀ (a : Nat) (b : α), (a, b) ∈ xs.enum → a + (n + 1) = a + 1 + n

Proof state:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (n : Nat), enumFrom n xs = map (Prod.map (fun x => x + n) id) xs.enum
n a : Nat
b : α
a✝ : (a, b) ∈ xs.enum
⊢ a + (n + 1) = a + 1 + n

Tactic:
exact (succ_add a n).symm

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ enumFrom n l = map (Prod.map (fun x => x + n) id) l.enum

Tactic:
induction l generalizing n with
| nil => simp
| cons x xs ih =>
  simp only [enumFrom_cons, ih, enum_cons, map_cons, Prod.map_apply, Nat.zero_add, id_eq, map_map,
    cons.injEq, map_inj_left, Function.comp_apply, Prod.forall, Prod.mk.injEq, and_true, true_and]
  intro a b _
  exact (succ_add a n).symm

Result:
no goals

Proof state:
case nil
α : Type u_1
n : Nat
⊢ enumFrom n [] = map (Prod.map (fun x => x + n) id) [].enum

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/CountableSeparatingOn.lean
theorem exists_subset_subsingleton_mem_of_forall_separating (p : Set α → Prop)
    {s : Set α} [h : HasCountableSeparatingOn α p s] (hs : s ∈ l)
    (hl : ∀ U, p U → U ∈ l ∨ Uᶜ ∈ l) : ∃ t, t ⊆ s ∧ t.Subsingleton ∧ t ∈ l

Proof state:
case intro.intro.intro.refine_2.inr
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s✝, ∀ y ∈ s✝, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ i ∈ S, iᶜ ∈ l → x ∉ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ i ∈ S, iᶜ ∈ l → y ∉ i
s : Set α
hsS : s ∈ S
hsl : sᶜ ∈ l
⊢ x ∈ s ↔ y ∈ s

Tactic:
simp only [hx.2 s hsS hsl, hy.2 s hsS hsl]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Monomial.lean
theorem monomial_natDegree_leadingCoeff_eq_self (h : #p.support ≤ 1) :
    monomial p.natDegree p.leadingCoeff = p

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : #p.support ≤ 1
⊢ (monomial p.natDegree) p.leadingCoeff = p

Tactic:
rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩

Result:
case intro.intro
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : #((monomial n) a).support ≤ 1
⊢ (monomial ((monomial n) a).natDegree) ((monomial n) a).leadingCoeff = (monomial n) a

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : #p.support ≤ 1
⊢ (monomial p.natDegree) p.leadingCoeff = p

Tactic:
classical
rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩
by_cases ha : a = 0 <;> simp [ha]

Result:
no goals

Proof state:
case intro.intro
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : #((monomial n) a).support ≤ 1
⊢ (monomial ((monomial n) a).natDegree) ((monomial n) a).leadingCoeff = (monomial n) a

Tactic:
by_cases ha : a = 0 <;> simp [ha]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Int.lean
theorem testBit_ofBits_lt {f : Fin n → Bool} (h : i < n) :
    (ofBits f).testBit i = f ⟨i, h⟩

Proof state:
case isFalse
n i : Nat
f : Fin n → Bool
h : i < n
h✝ : ¬2 * Nat.ofBits f < 2 ^ n
⊢ (subNatNat (Nat.ofBits f) (2 ^ n)).testBit i = f ⟨i, h⟩

Tactic:
have hlt := Nat.ofBits_lt_two_pow f

Result:
case isFalse
n i : Nat
f : Fin n → Bool
h : i < n
h✝ : ¬2 * Nat.ofBits f < 2 ^ n
hlt : Nat.ofBits f < 2 ^ n
⊢ (subNatNat (Nat.ofBits f) (2 ^ n)).testBit i = f ⟨i, h⟩

Proof state:
n i : Nat
f : Fin n → Bool
h : i < n
⊢ (ofBits f).testBit i = f ⟨i, h⟩

Tactic:
simp only [ofBits]

Result:
n i : Nat
f : Fin n → Bool
h : i < n
⊢ (if 2 * Nat.ofBits f < 2 ^ n then ofNat (Nat.ofBits f) else subNatNat (Nat.ofBits f) (2 ^ n)).testBit i = f ⟨i, h⟩

Proof state:
n i : Nat
f : Fin n → Bool
h : i < n
⊢ (if 2 * Nat.ofBits f < 2 ^ n then ofNat (Nat.ofBits f) else subNatNat (Nat.ofBits f) (2 ^ n)).testBit i = f ⟨i, h⟩

Tactic:
split

Result:
case isTrue
n i : Nat
f : Fin n → Bool
h : i < n
h✝ : 2 * Nat.ofBits f < 2 ^ n
⊢ (ofNat (Nat.ofBits f)).testBit i = f ⟨i, h⟩

case isFalse
n i : Nat
f : Fin n → Bool
h : i < n
h✝ : ¬2 * Nat.ofBits f < 2 ^ n
⊢ (subNatNat (Nat.ofBits f) (2 ^ n)).testBit i = f ⟨i, h⟩

Proof state:
case isFalse
n i : Nat
f : Fin n → Bool
h : i < n
h✝ : ¬2 * Nat.ofBits f < 2 ^ n
hlt : Nat.ofBits f < 2 ^ n
⊢ (subNatNat (Nat.ofBits f) (2 ^ n)).testBit i = f ⟨i, h⟩

Tactic:
simp [subNatNat_of_lt hlt, testBit, Nat.sub_sub, Nat.testBit_two_pow_sub_succ hlt, h]

Result:
no goals

Proof state:
case isTrue
n i : Nat
f : Fin n → Bool
h : i < n
h✝ : 2 * Nat.ofBits f < 2 ^ n
⊢ (ofNat (Nat.ofBits f)).testBit i = f ⟨i, h⟩

Tactic:
simp only [testBit, Nat.testBit_ofBits_lt, h]

Result:
no goals
-- Mathlib/Order/CompactlyGenerated/Intervals.lean
theorem isCompactElement {a : α} {b : Iic a} (h : CompleteLattice.IsCompactElement (b : α)) :
    CompleteLattice.IsCompactElement b

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
⊢ ∀ (ι : Type u_2) (s : ι → ↑(Iic a)), b ≤ iSup s → ∃ t, b ≤ ⨆ a_2 ∈ t, s a_2

Tactic:
intro ι s hb

Result:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : b ≤ iSup s
⊢ ∃ t, b ≤ ⨆ a_1 ∈ t, s a_1

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : ↑b ≤ iSup (Subtype.val ∘ s)
t : Finset ι
ht : ↑b ≤ ⨆ a_1 ∈ t, (Subtype.val ∘ s) a_1
⊢ ↑b ≤ (fun a_1 => ↑a_1) (⨆ a_1 ∈ t, s a_1)

Tactic:
simpa using ht

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : CompleteLattice.IsCompactElement ↑b
⊢ CompleteLattice.IsCompactElement b

Tactic:
simp only [CompleteLattice.isCompactElement_iff, Finset.sup_eq_iSup] at h ⊢

Result:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
⊢ ∀ (ι : Type u_2) (s : ι → ↑(Iic a)), b ≤ iSup s → ∃ t, b ≤ ⨆ a_2 ∈ t, s a_2

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : ↑b ≤ iSup (Subtype.val ∘ s)
⊢ ∃ t, b ≤ ⨆ a_1 ∈ t, s a_1

Tactic:
obtain ⟨t, ht⟩ := h ι ((↑) ∘ s) hb

Result:
case intro
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : ↑b ≤ iSup (Subtype.val ∘ s)
t : Finset ι
ht : ↑b ≤ ⨆ a_1 ∈ t, (Subtype.val ∘ s) a_1
⊢ ∃ t, b ≤ ⨆ a_1 ∈ t, s a_1

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : b ≤ iSup s
⊢ ∃ t, b ≤ ⨆ a_1 ∈ t, s a_1

Tactic:
replace hb : (b : α) ≤ iSup ((↑) ∘ s) := le_trans hb <| (coe_iSup s) ▸ le_refl _

Result:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : ↑b ≤ iSup (Subtype.val ∘ s)
⊢ ∃ t, b ≤ ⨆ a_1 ∈ t, s a_1

Proof state:
case intro
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : ↑b ≤ iSup (Subtype.val ∘ s)
t : Finset ι
ht : ↑b ≤ ⨆ a_1 ∈ t, (Subtype.val ∘ s) a_1
⊢ ∃ t, b ≤ ⨆ a_1 ∈ t, s a_1

Tactic:
exact ⟨t, (by simpa using ht : (b : α) ≤ _)⟩

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Index.lean
lemma Ideal.finite_quotient_pow (hI : I.FG) [Finite (R ⧸ I)] (n) : Finite (R ⧸ I ^ n)

Proof state:
case zero
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
hI : I.FG
inst✝ : Finite (R ⧸ I)
⊢ Finite (R ⧸ I ^ 0)

Tactic:
simp only [pow_zero, Ideal.one_eq_top]

Result:
case zero
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
hI : I.FG
inst✝ : Finite (R ⧸ I)
⊢ Finite (R ⧸ ⊤)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
hI : I.FG
inst✝ : Finite (R ⧸ I)
n : ℕ
⊢ Finite (R ⧸ I ^ n)

Tactic:
induction n with
| zero =>
  simp only [pow_zero, Ideal.one_eq_top]
  infer_instance
| succ n _ =>
  exact Submodule.finite_quotient_smul (I ^ n) hI

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
hI : I.FG
inst✝ : Finite (R ⧸ I)
⊢ Finite (R ⧸ ⊤)

Tactic:
infer_instance

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
hI : I.FG
inst✝ : Finite (R ⧸ I)
n : ℕ
a✝ : Finite (R ⧸ I ^ n)
⊢ Finite (R ⧸ I ^ (n + 1))

Tactic:
exact Submodule.finite_quotient_smul (I ^ n) hI

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem subset_image_iff [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} :
    t ⊆ s.image f ↔ ∃ s' : Finset α, s' ⊆ s ∧ s'.image f = t

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
⊢ t ⊆ image f s ↔ ∃ s' ⊆ s, image f s' = t

Tactic:
simp only [← coe_subset, coe_image, subset_set_image_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_surjective (h : Function.Surjective v) :
    Function.Surjective (linearCombination R v)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
h : Function.Surjective v
⊢ Function.Surjective ⇑(linearCombination R v)

Tactic:
intro x

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
h : Function.Surjective v
x : M
⊢ ∃ a, (linearCombination R v) a = x

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
h : Function.Surjective v
x : M
y : α
hy : v y = x
⊢ (linearCombination R v) (single y 1) = x

Tactic:
simp [hy]

Result:
no goals

Proof state:
case intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
h : Function.Surjective v
x : M
y : α
hy : v y = x
⊢ ∃ a, (linearCombination R v) a = x

Tactic:
exact ⟨Finsupp.single y 1, by simp [hy]⟩

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
h : Function.Surjective v
x : M
⊢ ∃ a, (linearCombination R v) a = x

Tactic:
obtain ⟨y, hy⟩ := h x

Result:
case intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
h : Function.Surjective v
x : M
y : α
hy : v y = x
⊢ ∃ a, (linearCombination R v) a = x
-- Mathlib/Algebra/Order/Floor/Div.lean
@[simp] lemma smul_floorDiv [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) (b : β) :
    a • b ⌊/⌋ a = b :=
  eq_of_forall_le_iff <| by simp [smul_le_smul_iff_of_pos_left, ha]

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : OrderedSemiring α
inst✝⁴ : OrderedAddCommMonoid β
inst✝³ : MulActionWithZero α β
inst✝² : FloorDiv α β
a : α
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : 0 < a
b : β
⊢ ∀ (c : β), c ≤ a • b ⌊/⌋ a ↔ c ≤ b

Tactic:
simp [smul_le_smul_iff_of_pos_left, ha]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem Real.logDeriv_sin : logDeriv (Real.sin) = Real.cot

Proof state:
⊢ logDeriv sin = cot

Tactic:
ext

Result:
case h
x✝ : ℝ
⊢ logDeriv sin x✝ = x✝.cot

Proof state:
case h
x✝ : ℝ
⊢ logDeriv sin x✝ = x✝.cot

Tactic:
rw [logDeriv, Real.deriv_sin, Pi.div_apply, Real.cot_eq_cos_div_sin]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem norm_image_of_norm_zero [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕) (hf : Continuous f) {x : E}
    (hx : ‖x‖ = 0) : ‖f x‖ = 0

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : FunLike 𝓕 E F
inst✝ : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf : Continuous ⇑f
x : E
hx : 0 ⤳ x
⊢ f 0 ⤳ f x

Tactic:
exact hx.map hf

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : FunLike 𝓕 E F
inst✝ : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf : Continuous ⇑f
x : E
hx : ‖x‖ = 0
⊢ ‖f x‖ = 0

Tactic:
rw [← mem_closure_zero_iff_norm, ← specializes_iff_mem_closure, ← map_zero f] at *

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : FunLike 𝓕 E F
inst✝ : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf : Continuous ⇑f
x : E
hx : 0 ⤳ x
⊢ f 0 ⤳ f x
-- Mathlib/Order/WellFoundedSet.lean
theorem wellFoundedOn_range : (range f).WellFoundedOn r ↔ WellFounded (r on f)

Proof state:
case mk.intro.refine_1
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ ∀ {a : β} {b : ↑(range f)}, r ↑b ↑(f' a) → ∃ c, f' c = b

Tactic:
rintro _ ⟨_, c', rfl⟩ -

Result:
case mk.intro.refine_1.mk.intro
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩
h : WellFounded (r on f)
c a✝ c' : β
⊢ ∃ c, f' c = ⟨f c', ⋯⟩

Proof state:
case mk.intro
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ Acc (fun a b => r ↑a ↑b) ⟨f c, ⋯⟩

Tactic:
refine Acc.of_downward_closed f' ?_ _ ?_

Result:
case mk.intro.refine_1
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ ∀ {a : β} {b : ↑(range f)}, r ↑b ↑(f' a) → ∃ c, f' c = b

case mk.intro.refine_2
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ Acc (InvImage (fun a b => r ↑a ↑b) f') c

Proof state:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩
⊢ (range f).WellFoundedOn r ↔ WellFounded (r on f)

Tactic:
refine ⟨fun h => (InvImage.wf f' h).mono fun c c' => id, fun h => ⟨?_⟩⟩

Result:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩
h : WellFounded (r on f)
⊢ ∀ (a : ↑(range f)), Acc (fun a b => r ↑a ↑b) a

Proof state:
case mk.intro.refine_2
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ Acc (InvImage (fun a b => r ↑a ↑b) f') c

Tactic:
exact h.apply _

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
⊢ (range f).WellFoundedOn r ↔ WellFounded (r on f)

Tactic:
let f' : β → range f := fun c => ⟨f c, c, rfl⟩

Result:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩
⊢ (range f).WellFoundedOn r ↔ WellFounded (r on f)

Proof state:
case mk.intro.refine_1.mk.intro
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩
h : WellFounded (r on f)
c a✝ c' : β
⊢ ∃ c, f' c = ⟨f c', ⋯⟩

Tactic:
exact ⟨c', rfl⟩

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩
h : WellFounded (r on f)
⊢ ∀ (a : ↑(range f)), Acc (fun a b => r ↑a ↑b) a

Tactic:
rintro ⟨_, c, rfl⟩

Result:
case mk.intro
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ Acc (fun a b => r ↑a ↑b) ⟨f c, ⋯⟩