harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/TwoSidedIdeal/BigOperators.lean
lemma listProd_mem {ι : Type*} (l : List ι) (f : ι → R) (hl : ∃ x ∈ l, f x ∈ I) :
    (l.map f).prod ∈ I

Proof state:
case cons
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
x : ι
l : List ι
ih : (∃ x ∈ l, f x ∈ I) → (List.map f l).prod ∈ I
hl : ∃ x_1 ∈ x :: l, f x_1 ∈ I
⊢ (List.map f (x :: l)).prod ∈ I

Tactic:
simp only [List.mem_cons, exists_eq_or_imp] at hl

Result:
case cons
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
x : ι
l : List ι
ih : (∃ x ∈ l, f x ∈ I) → (List.map f l).prod ∈ I
hl : f x ∈ I ∨ ∃ a ∈ l, f a ∈ I
⊢ (List.map f (x :: l)).prod ∈ I

Proof state:
case cons.inr
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
x : ι
l : List ι
ih : (∃ x ∈ l, f x ∈ I) → (List.map f l).prod ∈ I
hal : ∃ a ∈ l, f a ∈ I
⊢ (List.map f (x :: l)).prod ∈ I

Tactic:
simpa only [List.map_cons, List.prod_cons] using I.mul_mem_left _ _ <| ih hal

Result:
no goals

Proof state:
case cons
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
x : ι
l : List ι
ih : (∃ x ∈ l, f x ∈ I) → (List.map f l).prod ∈ I
hl : f x ∈ I ∨ ∃ a ∈ l, f a ∈ I
⊢ (List.map f (x :: l)).prod ∈ I

Tactic:
rcases hl with h | hal

Result:
case cons.inl
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
x : ι
l : List ι
ih : (∃ x ∈ l, f x ∈ I) → (List.map f l).prod ∈ I
h : f x ∈ I
⊢ (List.map f (x :: l)).prod ∈ I

case cons.inr
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
x : ι
l : List ι
ih : (∃ x ∈ l, f x ∈ I) → (List.map f l).prod ∈ I
hal : ∃ a ∈ l, f a ∈ I
⊢ (List.map f (x :: l)).prod ∈ I

Proof state:
case cons.inl
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
x : ι
l : List ι
ih : (∃ x ∈ l, f x ∈ I) → (List.map f l).prod ∈ I
h : f x ∈ I
⊢ (List.map f (x :: l)).prod ∈ I

Tactic:
simpa only [List.map_cons, List.prod_cons] using I.mul_mem_right _ _ h

Result:
no goals

Proof state:
case nil
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
hl : ∃ x ∈ [], f x ∈ I
⊢ (List.map f []).prod ∈ I

Tactic:
simp only [List.not_mem_nil, false_and, exists_false] at hl

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

Proof state:
m : ℤ
x : ℝ
⊢ Irrational (↑m * x) ↔ m ≠ 0 ∧ Irrational x

Tactic:
rw [← cast_intCast, irrational_rat_mul_iff, Int.cast_ne_zero]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeries.term_smul_apply (f : ℕ → ℂ) (c s : ℂ) (n : ℕ) :
    term (c • f) s n = c * term f s n

Proof state:
f : ℕ → ℂ
c s : ℂ
n : ℕ
⊢ term (c • f) s n = c * term f s n

Tactic:
simp [term_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem index_nonempty (b : Basis ι R M) [Nontrivial M] : Nonempty ι

Proof state:
case intro.intro.intro
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Nontrivial M
x y : M
ne : x ≠ y
i : ι
h✝ : ¬(b.repr x) i = (b.repr y) i
⊢ Nonempty ι

Tactic:
exact ⟨i⟩

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Nontrivial M
⊢ Nonempty ι

Tactic:
obtain ⟨x, y, ne⟩ : ∃ x y : M, x ≠ y := Nontrivial.exists_pair_ne

Result:
case intro.intro
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Nontrivial M
x y : M
ne : x ≠ y
⊢ Nonempty ι

Proof state:
case intro.intro
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Nontrivial M
x y : M
ne : x ≠ y
⊢ Nonempty ι

Tactic:
obtain ⟨i, _⟩ := not_forall.mp (mt b.ext_elem_iff.2 ne)

Result:
case intro.intro.intro
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Nontrivial M
x y : M
ne : x ≠ y
i : ι
h✝ : ¬(b.repr x) i = (b.repr y) i
⊢ Nonempty ι
-- Mathlib/GroupTheory/PushoutI.lean
theorem ofCoprodI_of (i : ι) (g : G i) :
    (ofCoprodI (CoprodI.of g) : PushoutI φ) = of i g

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
g : G i
⊢ ofCoprodI (CoprodI.of g) = (of i) g

Tactic:
simp [ofCoprodI]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_mono_left {m : MeasurableSpace α} (T T' : Set α → F →L[ℝ] G'')
    (hTT' : ∀ s x, T s x ≤ T' s x) (f : α →ₛ F) : setToSimpleFunc T f ≤ setToSimpleFunc T' f

Proof state:
α : Type u_1
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G'' : Type u_8
inst✝¹ : NormedLatticeAddCommGroup G''
inst✝ : NormedSpace ℝ G''
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] G''
hTT' : ∀ (s : Set α) (x : F), (T s) x ≤ (T' s) x
f : α →ₛ F
⊢ setToSimpleFunc T f ≤ setToSimpleFunc T' f

Tactic:
simp_rw [setToSimpleFunc]

Result:
α : Type u_1
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G'' : Type u_8
inst✝¹ : NormedLatticeAddCommGroup G''
inst✝ : NormedSpace ℝ G''
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] G''
hTT' : ∀ (s : Set α) (x : F), (T s) x ≤ (T' s) x
f : α →ₛ F
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x ≤ ∑ x ∈ f.range, (T' (⇑f ⁻¹' {x})) x

Proof state:
α : Type u_1
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G'' : Type u_8
inst✝¹ : NormedLatticeAddCommGroup G''
inst✝ : NormedSpace ℝ G''
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] G''
hTT' : ∀ (s : Set α) (x : F), (T s) x ≤ (T' s) x
f : α →ₛ F
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x ≤ ∑ x ∈ f.range, (T' (⇑f ⁻¹' {x})) x

Tactic:
exact sum_le_sum fun i _ => hTT' _ i

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_smul_sub_right (x y : V) (r : ℝ) :
    (o.oangle x (r • x - y)).sign = -(o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
⊢ (o.oangle x (r • x - y)).sign = -(o.oangle x y).sign

Tactic:
rw [← oangle_sign_neg_right, sub_eq_add_neg, oangle_sign_smul_add_right]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean
theorem HasStrictDerivAt.clog_real {f : ℝ → ℂ} {x : ℝ} {f' : ℂ} (h₁ : HasStrictDerivAt f f' x)
    (h₂ : f x ∈ slitPlane) : HasStrictDerivAt (fun t => log (f t)) (f' / f x) x

Proof state:
f : ℝ → ℂ
x : ℝ
f' : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun t => log (f t)) (f' / f x) x

Tactic:
simpa only [div_eq_inv_mul] using (hasStrictFDerivAt_log_real h₂).comp_hasStrictDerivAt x h₁

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The arithmetic function associated to a Dirichlet character is multiplicative. -/
lemma isMultiplicative_toArithmeticFunction {N : ℕ} {R : Type*} [CommMonoidWithZero R]
    (χ : DirichletCharacter R N) :
    (toArithmeticFunction (χ ·)).IsMultiplicative

Proof state:
N : ℕ
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R N
⊢ (toArithmeticFunction fun x => χ ↑x).IsMultiplicative

Tactic:
refine IsMultiplicative.iff_ne_zero.mpr ⟨?_, fun {m} {n} hm hn _ ↦ ?_⟩

Result:
case refine_1
N : ℕ
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R N
⊢ (toArithmeticFunction fun x => χ ↑x) 1 = 1

case refine_2
N : ℕ
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R N
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
x✝ : m.Coprime n
⊢ (toArithmeticFunction fun x => χ ↑x) (m * n) =
    (toArithmeticFunction fun x => χ ↑x) m * (toArithmeticFunction fun x => χ ↑x) n

Proof state:
case refine_2
N : ℕ
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R N
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
x✝ : m.Coprime n
⊢ (toArithmeticFunction fun x => χ ↑x) (m * n) =
    (toArithmeticFunction fun x => χ ↑x) m * (toArithmeticFunction fun x => χ ↑x) n

Tactic:
simp [toArithmeticFunction, hm, hn]

Result:
no goals

Proof state:
case refine_1
N : ℕ
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R N
⊢ (toArithmeticFunction fun x => χ ↑x) 1 = 1

Tactic:
simp [toArithmeticFunction]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem iUnion_smul_eq_setOf_exists {s : Set β} : ⋃ g : α, g • s = { a | ∃ g : α, g • a ∈ s }

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ ⋃ g, g • s = {a | ∃ g, g • a ∈ s}

Tactic:
simp_rw [← iUnion_setOf, ← iUnion_inv_smul, ← preimage_smul, preimage]

Result:
no goals
-- Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
theorem Ideal.minimalPrimes_eq_empty_iff (I : Ideal R) :
    I.minimalPrimes = ∅ ↔ I = ⊤

Proof state:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
⊢ False

Tactic:
have ⟨p, hp⟩ := Ideal.exists_minimalPrimes_le hM'

Result:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
p : Ideal R
hp : p ∈ I.minimalPrimes ∧ p ≤ M
⊢ False

Proof state:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
⊢ False

Tactic:
have ⟨M, hM, hM'⟩ := Ideal.exists_le_maximal I h

Result:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
⊢ False

Proof state:
case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I = ⊤ → I.minimalPrimes = ∅

Tactic:
rintro rfl

Result:
case mpr
R : Type u_1
inst✝ : CommSemiring R
⊢ ⊤.minimalPrimes = ∅

Proof state:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
p : Ideal R
hp : p ∈ ∅ ∧ p ≤ M
⊢ False

Tactic:
apply Set.not_mem_empty _ hp.1

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.minimalPrimes = ∅ ↔ I = ⊤

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.minimalPrimes = ∅ → I = ⊤

case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I = ⊤ → I.minimalPrimes = ∅

Proof state:
case mpr
R : Type u_1
inst✝ : CommSemiring R
⊢ ⊤.minimalPrimes = ∅

Tactic:
exact Ideal.minimalPrimes_top

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.minimalPrimes = ∅ → I = ⊤

Tactic:
intro e

Result:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
⊢ I = ⊤

Proof state:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
p : Ideal R
hp : p ∈ I.minimalPrimes ∧ p ≤ M
⊢ False

Tactic:
rw [e] at hp

Result:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
p : Ideal R
hp : p ∈ ∅ ∧ p ≤ M
⊢ False

Proof state:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
⊢ I = ⊤

Tactic:
by_contra h

Result:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
⊢ False
-- Mathlib/Algebra/Group/End.lean
@[simp] lemma zpow_addRight : ∀ (n : ℤ), Equiv.addRight a ^ n = Equiv.addRight (n • a)
  | Int.ofNat n => by simp
  | Int.negSucc n => by simp

Proof state:
α : Type u_4
inst✝ : AddGroup α
a : α
n : ℕ
⊢ Equiv.addRight a ^ Int.negSucc n = Equiv.addRight (Int.negSucc n • a)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_4
inst✝ : AddGroup α
a : α
n : ℕ
⊢ Equiv.addRight a ^ Int.ofNat n = Equiv.addRight (Int.ofNat n • a)

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/Measure.lean
theorem volume_iUnion_setOf_liouvilleWith :
    volume (⋃ (p : ℝ) (_hp : 2 < p), { x : ℝ | LiouvilleWith p x }) = 0

Proof state:
m : ℤ
⊢ volume (⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0

Tactic:
clear m

Result:
⊢ volume (⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0

Proof state:
⊢ ∀ (i : ℤ),
    volume
        ((fun x => x + ↑i) ⁻¹'
          ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
      0

Tactic:
intro m

Result:
m : ℤ
⊢ volume
      ((fun x => x + ↑m) ⁻¹'
        ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0

Proof state:
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 + 1 / ↑n = r
⊢ volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0

Tactic:
replace hr : 2 < r := by simp [← hr, zero_lt_one.trans_le hn]

Result:
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 < r
⊢ volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0

Proof state:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), volume (⋃ a ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ Summable fun a => 2 * (↑a ^ (1 - r) + ↑a ^ (-r))

Tactic:
refine (Summable.add ?_ ?_).mul_left _ <;> simp only [NNReal.summable_rpow] <;> linarith

Result:
no goals

Proof state:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
⊢ ∑ a ∈ Finset.Icc 0 ↑b, volume (B a b) = ↑((↑b + 1) * (2 / ↑b ^ r))

Tactic:
simp only [hB, Int.card_Icc, Finset.sum_const, nsmul_eq_mul, sub_zero, ← Int.ofNat_succ,
  Int.toNat_natCast, ← Nat.cast_succ, ENNReal.coe_mul, ENNReal.coe_natCast]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem QuotientAddGroup.norm_mk {S : AddSubgroup M} (x : M) :
    ‖(x : M ⧸ S)‖ = infDist x S

Proof state:
case e_s.h
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x y : M
⊢ y ∈ ⇑(IsometryEquiv.subLeft x).symm ⁻¹' {m | ↑m = ↑x} ↔ y ∈ ↑S

Tactic:
simp only [mem_preimage, IsometryEquiv.subLeft_symm_apply, mem_setOf_eq, QuotientAddGroup.eq,
  neg_add, neg_neg, neg_add_cancel_right, SetLike.mem_coe]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M
⊢ infDist x (⇑(IsometryEquiv.subLeft x).symm ⁻¹' {m | ↑m = ↑x}) = infDist x ↑S

Tactic:
congr 1 with y

Result:
case e_s.h
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x y : M
⊢ y ∈ ⇑(IsometryEquiv.subLeft x).symm ⁻¹' {m | ↑m = ↑x} ↔ y ∈ ↑S

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M
⊢ ‖↑x‖ = infDist x ↑S

Tactic:
rw [norm_eq_infDist, ← infDist_image (IsometryEquiv.subLeft x).isometry,
  IsometryEquiv.subLeft_apply, sub_zero, ← IsometryEquiv.preimage_symm]

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M
⊢ infDist x (⇑(IsometryEquiv.subLeft x).symm ⁻¹' {m | ↑m = ↑x}) = infDist x ↑S
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem mem_zipIdx' {x : α} {i : Nat} {xs : Vector α n} (h : (x, i) ∈ xs.zipIdx) :
    i < n ∧ x = xs[i]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) :=
  ⟨by simpa using snd_lt_add_of_mem_zipIdx h, fst_eq_of_mem_zipIdx h⟩

Proof state:
α : Type ?u.29053
n : Nat
x : α
i : Nat
xs : Vector α n
h : (x, i) ∈ xs.zipIdx
this : 0 ≤ (x, i).snd
⊢ i < n

Tactic:
have := snd_lt_add_of_mem_zipIdx h

Result:
α : Type ?u.29053
n : Nat
x : α
i : Nat
xs : Vector α n
h : (x, i) ∈ xs.zipIdx
this✝ : 0 ≤ (x, i).snd
this : (x, i).snd < 0 + n
⊢ i < n

Proof state:
α : Type ?u.29053
n : Nat
x : α
i : Nat
xs : Vector α n
h : (x, i) ∈ xs.zipIdx
⊢ i < n

Tactic:
have := le_snd_of_mem_zipIdx h

Result:
α : Type ?u.29053
n : Nat
x : α
i : Nat
xs : Vector α n
h : (x, i) ∈ xs.zipIdx
this : 0 ≤ (x, i).snd
⊢ i < n

Proof state:
α : Type u_1
n : Nat
x : α
i : Nat
xs : Vector α n
h : (x, i) ∈ xs.zipIdx
⊢ i < n

Tactic:
simpa using snd_lt_add_of_mem_zipIdx h

Result:
no goals

Proof state:
α : Type ?u.29053
n : Nat
x : α
i : Nat
xs : Vector α n
h : (x, i) ∈ xs.zipIdx
this✝ : 0 ≤ (x, i).snd
this : (x, i).snd < 0 + n
⊢ i < n

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/Algebra/Module/CharacterSpace.lean
theorem ext_ker {φ ψ : characterSpace 𝕜 A} (h : RingHom.ker φ = RingHom.ker ψ) : φ = ψ

Proof state:
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
⊢ φ x = ψ x

Tactic:
have : x - algebraMap 𝕜 A (ψ x) ∈ RingHom.ker φ := by
  simpa only [h, RingHom.mem_ker, map_sub, AlgHomClass.commutes] using sub_self (ψ x)

Result:
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
this : x - (algebraMap 𝕜 A) (ψ x) ∈ RingHom.ker φ
⊢ φ x = ψ x

Proof state:
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
this : x - (algebraMap 𝕜 A) (ψ x) ∈ RingHom.ker φ
⊢ φ x = ψ x

Tactic:
rwa [RingHom.mem_ker, map_sub, AlgHomClass.commutes, sub_eq_zero] at this

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
⊢ φ = ψ

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
⊢ φ x = ψ x

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
⊢ x - (algebraMap 𝕜 A) (ψ x) ∈ RingHom.ker φ

Tactic:
simpa only [h, RingHom.mem_ker, map_sub, AlgHomClass.commutes] using sub_self (ψ x)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma preΨ_ne_zero [Nontrivial R] {n : ℤ} (h : (n : R) ≠ 0) : W.preΨ n ≠ 0

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℕ
h : ↑↑n ≠ 0
⊢ ↑n ≠ 0

Tactic:
exact_mod_cast h

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
h : ↑n ≠ 0
⊢ W.preΨ n ≠ 0

Tactic:
induction n using Int.negInduction with
| nat n => simpa only [preΨ_ofNat] using W.preΨ'_ne_zero <| by exact_mod_cast h
| neg ih n => simpa only [preΨ_neg, neg_ne_zero]
      using ih n <| neg_ne_zero.mp <| by exact_mod_cast h

Result:
no goals

Proof state:
case nat
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℕ
h : ↑↑n ≠ 0
⊢ W.preΨ ↑n ≠ 0

Tactic:
simpa only [preΨ_ofNat] using W.preΨ'_ne_zero <| by exact_mod_cast h

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
ih : ∀ (n : ℕ), ↑↑n ≠ 0 → W.preΨ ↑n ≠ 0
n : ℕ
h : ↑(-↑n) ≠ 0
⊢ -↑↑n ≠ 0

Tactic:
exact_mod_cast h

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
ih : ∀ (n : ℕ), ↑↑n ≠ 0 → W.preΨ ↑n ≠ 0
n : ℕ
h : ↑(-↑n) ≠ 0
⊢ W.preΨ (-↑n) ≠ 0

Tactic:
simpa only [preΨ_neg, neg_ne_zero]
using ih n <| neg_ne_zero.mp <| by exact_mod_cast h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem ofNat_natAbs (a : Int) : (a.natAbs : Int) = if 0 ≤ a then a else -a

Proof state:
case h_2
n✝ : Int
n : Nat
⊢ ↑n.succ = if 0 ≤ Int.negSucc n then Int.negSucc n else -Int.negSucc n

Tactic:
simp

Result:
case h_2
n✝ : Int
n : Nat
⊢ ↑n + 1 = -Int.negSucc n

Proof state:
case h_1
n✝ : Int
n : Nat
⊢ ↑n = if 0 ≤ Int.ofNat n then Int.ofNat n else -Int.ofNat n

Tactic:
simp only [Int.ofNat_eq_coe]

Result:
case h_1
n✝ : Int
n : Nat
⊢ ↑n = if 0 ≤ ↑n then ↑n else -↑n

Proof state:
case h_1
n✝ : Int
n : Nat
⊢ ↑n = if 0 ≤ ↑n then ↑n else -↑n

Tactic:
rw [if_pos (Int.ofNat_nonneg n)]

Result:
no goals

Proof state:
a : Int
⊢ ↑(match a with
      | Int.ofNat m => m
      | Int.negSucc m => m.succ) =
    if 0 ≤ a then a else -a

Tactic:
split <;> rename_i n

Result:
case h_1
n✝ : Int
n : Nat
⊢ ↑n = if 0 ≤ Int.ofNat n then Int.ofNat n else -Int.ofNat n

case h_2
n✝ : Int
n : Nat
⊢ ↑n.succ = if 0 ≤ Int.negSucc n then Int.negSucc n else -Int.negSucc n

Proof state:
case h_2
n✝ : Int
n : Nat
⊢ ↑n + 1 = -Int.negSucc n

Tactic:
rfl

Result:
no goals

Proof state:
a : Int
⊢ ↑a.natAbs = if 0 ≤ a then a else -a

Tactic:
rw [Int.natAbs.eq_def]

Result:
a : Int
⊢ ↑(match a with
      | Int.ofNat m => m
      | Int.negSucc m => m.succ) =
    if 0 ≤ a then a else -a
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_union {s t : Set E} :
    IsVonNBounded 𝕜 (s ∪ t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
s t : Set E
⊢ IsVonNBounded 𝕜 (s ∪ t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
simp only [IsVonNBounded, absorbs_union, forall_and]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem replicate_sublist_replicate {m n} (a : α) :
    replicate m a <+ replicate n a ↔ m ≤ n

Proof state:
case refine_1
α : Type u_1
m n : Nat
a : α
h : replicate m a <+ replicate n a
this : (replicate m a).length ≤ (replicate n a).length
⊢ m ≤ n

Tactic:
simp only [length_replicate] at this ⊢

Result:
case refine_1
α : Type u_1
m n : Nat
a : α
h : replicate m a <+ replicate n a
this : m ≤ n
⊢ m ≤ n

Proof state:
case refine_2.step
α : Type u_1
m n : Nat
a : α
m✝ : Nat
a✝ : m.le m✝
a_ih✝ : replicate m a <+ replicate m✝ a
⊢ replicate m a <+ replicate m✝.succ a

Tactic:
simp [*, replicate, Sublist.cons]

Result:
no goals

Proof state:
α : Type u_1
m n : Nat
a : α
⊢ replicate m a <+ replicate n a ↔ m ≤ n

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

Result:
case refine_1
α : Type u_1
m n : Nat
a : α
h : replicate m a <+ replicate n a
⊢ m ≤ n

case refine_2
α : Type u_1
m n : Nat
a : α
h : m ≤ n
⊢ replicate m a <+ replicate n a

Proof state:
case refine_2.refl
α : Type u_1
m n : Nat
a : α
⊢ replicate m a <+ replicate m a

Tactic:
apply Sublist.refl

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m n : Nat
a : α
h : m ≤ n
⊢ replicate m a <+ replicate n a

Tactic:
induction h with
| refl => apply Sublist.refl
| step => simp [*, replicate, Sublist.cons]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m n : Nat
a : α
h : replicate m a <+ replicate n a
⊢ m ≤ n

Tactic:
have := h.length_le

Result:
case refine_1
α : Type u_1
m n : Nat
a : α
h : replicate m a <+ replicate n a
this : (replicate m a).length ≤ (replicate n a).length
⊢ m ≤ n

Proof state:
case refine_1
α : Type u_1
m n : Nat
a : α
h : replicate m a <+ replicate n a
this : m ≤ n
⊢ m ≤ n

Tactic:
exact this

Result:
no goals